mathlib-bors[bot]

Results 216 comments of mathlib-bors[bot]
trafficstars

feat: `lake exe mk_all` as a Lean executable

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

refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents

:v: mans0954 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).

refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents

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

perf: improves the performance of the `Repr (Equiv.Perm α)` instance

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

feat: index Chebyshev polynomials by integers instead of natural numbers

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

feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring

:v: mans0954 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(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring

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

refactor: change the format of `Repr (Equiv.Perm α)` from `{c[0, 1], c[2, 3]}` to `c[0, 1] * c[2, 3]`

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

refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings

:v: mans0954 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).

refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings

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