Commit 2023-09-18 15:32 86fa7890

feat: TwoUniqueProds (#7169)

• Introduce TwoUniqueProds/Sums: let R[G] be a monoid algebra over a semiring R without zero-divisors. A natural sufficient condition for R[G] to have no zero-divisors is that G has UniqueProds, as is shown by MonoidAlgebra.instNoZeroDivisorsOfUniqueProds. Similarly, a natural sufficient condition for R[G] to have only trivial units (of the form rg with r a unit in R and g a unit in G) is that G has TwoUniqueProds, but we don't prove this yet in this PR. TwoUniqueProds G is also a natural sufficient condition in order for factors of a homogeneous element in an algebra graded by G without zero-divisors to themselves be homogeneous.
• Show TwoUniqueProds implies UniqueProds: TwoUniqueProds.toUniqueProds
• Strengthen of_Covariant_right/left to have TwoUniqueProds as conclusion
• Extract of_image_filter from the proof of the instance UniqueProds (∀ i, G i) and use it also in the proof of TwoUniqueProds (∀ i, G i)
• Use some private defs (starting from private abbrev I) to transfer (Two)UniqueProds (∀ i, G i) instances to (Two)UniqueProds (G × H)
• Move the [Module ℚ G] : UniqueSums G instance from NoZeroDivisors.lean to UniqueProds.lean and strengthen to TwoUniqueSums New lemmas about UniqueMul:
• of_card_le_one, iff_card_le_one, UniqueMul_of_TwoUniqueMul