Theorem MonoidAlgebra.domCongr_comp_lsingle

Modification history

2025-08-31 00:30

Mathlib/Algebra/MonoidAlgebra/Basic.lean

chore(Algebra/MonoidAlgebra): use `to_additive` for `AddMonoidAlgebra` (#29036) …

Modified MonoidAlgebra.domCongr_comp_lsingle View on Github →

2025-05-11 12:20

Mathlib/Algebra/MonoidAlgebra/Basic.lean

feat(MonoidAlgebra): `domCongr` preserves `lsingle` (#24768) …

Added MonoidAlgebra.domCongr_comp_lsingle View on Github →