Commit 2023-03-17 12:26 70467354

View on Github →

feat: port Algebra.MonoidAlgebra.NoZeroDivisors (#2938)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

added theorem AddMonoidAlgebra.Left.exists_add_of_mem_support_single_mul

added theorem AddMonoidAlgebra.NoZeroDivisors.of_left_ordered

added theorem AddMonoidAlgebra.NoZeroDivisors.of_right_ordered

added theorem AddMonoidAlgebra.Right.exists_add_of_mem_support_single_mul

added theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne