Theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd

Modification history

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_uniqueAdd View 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_uniqueAdd View on Github →