Theorem MonoidAlgebra.commRingEquiv_single_one

Modification history

2026-04-13 11:55
Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
feat(Algebra/MonoidAlgebra): a few lemmas (#37750) …
Added MonoidAlgebra.commRingEquiv_single_oneView on Github →