Theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd

Modification history

2025-12-05 12:39
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
chore(Algebra/MonoidAlgebra): use `to_additive` more (#32398) …
Deleted AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAddView on Github →
2023-09-16 19:24
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
feat(AddMonoidAlgebra*): add notation `R[A]` for `addMonoidAlgebra R A` (#7203) …
Modified AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAddView on Github →
2023-09-14 18:26
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
feat(UniqueProds + NoZeroDivisors): AddMonoidAlgebra instances (#6723) …
Added AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAddView on Github →