Commit 2026-04-13 11:55 60a9c91d

View on Github →

feat(Algebra/MonoidAlgebra): a few lemmas (#37750) Miscellaneous lemmas I need on my way to the big refactor in #25273.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem MonoidAlgebra.commAlgEquiv_single_one

added theorem MonoidAlgebra.commAlgEquiv_single_one_single

added theorem MonoidAlgebra.toRingEquiv_symm_uniqueAlgEquiv

added theorem MonoidAlgebra.toRingEquiv_uniqueAlgEquiv

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added theorem MonoidAlgebra.commRingEquiv_single_one

added theorem MonoidAlgebra.commRingEquiv_single_one_single

deleted theorem MonoidAlgebra.map_neg

deleted theorem MonoidAlgebra.map_sub