mathlib4

mathlib4 copied to clipboard

feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals

2

--- - [ ] depends on: #14456 [](https://gitpod.io/from-referrer/)

jjaassoonn

feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals

2

--- [](https://gitpod.io/from-referrer/)

jjaassoonn

feat(ENNReal/Real): +1 `@[gcongr]`, +2 lemmas

1

--- [](https://gitpod.io/from-referrer/)

urkud

doc: add reassoc docstring

1

Add docstring for `@[reassoc]` attribute. --- [](https://gitpod.io/from-referrer/) Note that, in contrast to when I'm adding maths docstrings, here I know far less about what I'm talking about (in...

kbuzzard

feat(RingTheory/TwoSidedIdeal/Basic): two-sided-ideal as a bimodule

1

--- [](https://gitpod.io/from-referrer/)

jjaassoonn

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

3

This PR shows that if the centroid of a *-ring is commutative then it is a *-ring. Previously submitted to mathlib as https://github.com/leanprover-community/mathlib/pull/18096 --- - [x] depends on: #6562 -...

mans0954

feat: symmetric monoidal structure on graded objects

2

--- (Refactor of #6379) This is a draft. It shall be split in separate PR later: - [ ] depends on: #14457 - [ ] depends on: #14343 - [x]...

joelriou

feat: Lindemann-Weierstrass Theorem

5

--- There's still a lot of work to be done before it gets into mathlib. - [x] depends on: #6593 - [x] depends on: #6719 - [x] depends on: #6723...

astrainfinita

feat (RingTheory.MvPowerSeries.Inverse)

1

Prove properties of the inverse of a power series over a general Ring. A power series is a unit iff its constant coefficient is a unit. If its constant coefficient...

AntoineChambert-Loir

feat(Analysis/LocallyConvex/Polar): Calculate the polar of a set closed under scalar multiplication

1

The polar of a set closed under scalar multiplication the set of functionals vanishing on the set. In particular this applies to submodules. --- [](https://gitpod.io/from-referrer/)

mans0954