Theorem MonoidAlgebra.toRingEquiv_symm_uniqueAlgEquiv

Modification history

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