Commit 2023-09-14 18:26 96d78537

View on Github →

feat(UniqueProds + NoZeroDivisors): AddMonoidAlgebra instances (#6723) Add UniqueProds/Sums and NoZeroDivisors instances. This has recently been prompted by the port of the Lindemann-Weierstrass Theorem, but the results are self-contained. Instances such as the ones in this PR are the reasons why UniqueProds/Sums were introduced. Affected files:

Algebra/
	Group/UniqueProds.lean
	MonoidAlgebra/NoZeroDivisors.lean

Estimated changes

Modified Mathlib/Algebra/Group/UniqueProds.lean

deleted theorem UniqueProds.iff_mulOpposite

added theorem UniqueProds.mulHom_image_iff

added theorem UniqueProds.mulHom_image_of_injective

modified theorem UniqueProds.of_mulOpposite

deleted theorem UniqueProds.of_subsingleton

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

deleted theorem AddMonoidAlgebra.Left.exists_add_of_mem_support_single_mul

deleted theorem AddMonoidAlgebra.NoZeroDivisors.of_left_ordered

deleted theorem AddMonoidAlgebra.NoZeroDivisors.of_right_ordered

deleted theorem AddMonoidAlgebra.Right.exists_add_of_mem_support_single_mul

deleted theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne

added theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd

added theorem MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul