leanprover-community-mathlib4-bot

Results 107 comments of leanprover-community-mathlib4-bot

feat: the root space of a Coxeter group and the bilinear form on it

This PR/issue depends on: * ~~leanprover-community/mathlib4#11436~~ * leanprover-community/mathlib4#11465 By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat: add length, reduced words in Coxeter groups

This PR/issue depends on: * ~~leanprover-community/mathlib4#11406~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

Make MonadControlT the transitive closure of MonadControl

- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-16 21:30:15)

fix: don't write padding bits to olean files

- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-19 05:26:41) - ✅ Mathlib branch [lean-pr-testing-2908](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-2908) has successfully built against this PR....

feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`

This PR/issue depends on: * leanprover-community/mathlib4#11155 By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat: `pp.parens` option to pretty print with all parentheses

- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-20' branch does not exist there yet. We will retry when you push more commits. It may be necessary...

feat(CategoryTheory/Triangulated): homological functors

This PR/issue depends on: * ~~leanprover-community/mathlib4#11740~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat: make constructor tactic fail in ambiguous cases

- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet. We will retry when you push more commits. It may be necessary...

doc: mention maxSteps setting in its error message

Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)): - ❗ Std/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. (2024-02-09 04:41:18)

fix: collect level parameters in evalExpr

- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-18 15:50:28) - ✅ Mathlib branch [lean-pr-testing-3090](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3090) has successfully built against this PR....