mathlib-bors[bot]

Results 214 comments of mathlib-bors[bot]

feat: `subsingleton` tactic

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9750613906/job/26910399546) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9750613906/job/26910399163)

Feat(LinearAlgebra/TensorProduct/RightExactness): Tensoring with a quotient of the ring

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730857) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730644) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730792)

feat: add lemma `List.prod_map_ite_eq`

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9843202754/job/27173886749) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9843202754/job/27173886185)

feat(MeasureTheory): generalize `ae` to `OuterMeasureClass`

:v: urkud can now approve this pull request. To approve and merge a pull request, simply reply with `bors r+`. More detailed instructions are available [here](https://bors.tech/documentation/getting-started/#reviewing-pull-requests).

feat(MeasureTheory): generalize `ae` to `OuterMeasureClass`

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9271030718/job/25505466021) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9271030718/job/25505466395) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9271030718/job/25505465325)

feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot

:v: acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with `bors r+`. More detailed instructions are available [here](https://bors.tech/documentation/getting-started/#reviewing-pull-requests).

feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9223337265/job/25376330710) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9223337265/job/25376330054) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9223337265/job/25376330364)

feat: syntax linter for `#`-commands

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730857) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730644) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9218346948/job/25361730792)

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial): compute degrees of division polynomials

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9551011773/job/26324363000) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9551011773/job/26324362682)

feat: trace of a permutation matrix

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9235533804/job/25410445038) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9235533804/job/25410444621) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9235533804/job/25410444804)