mathlib-bors[bot]

Results 216 comments of mathlib-bors[bot]
trafficstars

feat(Topology/Algebra/Algebra): add ContinuousAlgHom

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

feat(Order/Filer/ENNReal): add Real.limsup_mul_le

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

feat(algebra/hom/centroid): Commutative Centroid of a *-ring is a *-ring

: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/hom/centroid): Commutative Centroid of a *-ring is a *-ring

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

refactor(LinearAlgebra/BilinForm): Remove `structure BilinForm` from Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

: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/BilinForm): Remove `structure BilinForm` from Mathlib, migrate all of `_root_.BilinForm` to `LinearMap.BilinForm`

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

chore: Split `RingTheory.Trace` and `RingTheory.Norm`

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

refactor(Topology/Category): refactor Stonean.Basic

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

feat(Condensed): characterisation of discrete (light) condensed sets and modules

:v: dagurtomas 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(Condensed): characterisation of discrete (light) condensed sets and modules

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