Commit 2025-07-05 05:16 84910edb

View on Github →

feat(Algebra/Pi): add various AlgEquivs and RingEquivs (#24520) Add

RingEquiv.sumArrowEquivProdArrow: ring version of Equiv.sumArrowEquivProdArrow.
AlgEquiv.sumArrowEquivProdArrow: algebra version of Equiv.sumArrowEquivProdArrow.
AlgEquiv.piCongrLeft': algebra version of Equiv.piCongrLeft.
AlgEquiv.piCongrLeft: algebra version of Equiv.piCongrLeft.
AlgEquiv.funUnique: algebra version of Equiv.funUnique.
AlgEquiv.prodCongr: algebra version of Equiv.prodCongr. The four last ones already have ring versions.

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

added def AlgEquiv.funUnique

added theorem AlgEquiv.funUnique_apply

added theorem AlgEquiv.funUnique_symm_apply

added def AlgEquiv.piCongrLeft'

added theorem AlgEquiv.piCongrLeft'_apply

added theorem AlgEquiv.piCongrLeft'_symm_apply

added def AlgEquiv.piCongrLeft

added theorem AlgEquiv.piCongrLeft_apply

added theorem AlgEquiv.piCongrLeft_symm_apply

added def AlgEquiv.sumArrowEquivProdArrow

added theorem AlgEquiv.sumArrowEquivProdArrow_apply

added theorem AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr

Modified Mathlib/Algebra/Algebra/Prod.lean

added def AlgEquiv.prodCongr

added theorem AlgEquiv.prodCongr_apply

added theorem AlgEquiv.prodCongr_symm_apply

Modified Mathlib/Algebra/Ring/Equiv.lean

added def RingEquiv.sumArrowEquivProdArrow

added theorem RingEquiv.sumArrowEquivProdArrow_apply

added theorem RingEquiv.sumArrowEquivProdArrow_symm_apply