Theorem MonoidAlgebra.single_commute

Modification history

2024-09-16 14:35

Mathlib/Algebra/MonoidAlgebra/Basic.lean

chore: split Algebra.MonoidAlgebra.Basic (#16531) …

Modified MonoidAlgebra.single_commute View on Github →

2023-12-17 20:09

Mathlib/Algebra/MonoidAlgebra/Basic.lean

feat(Algebra/MonoidAlgebra): when `single` and `of` commute (#8975) …

Added MonoidAlgebra.single_commute View on Github →