Commit 2024-10-04 14:05 5e050d47

View on Github →

chore(*): assume Subsingleton Mˣ instead of Unique Mˣ (#17391) Also drop a Nontrivial assumption in 1 lemma.

Estimated changes

Modified Mathlib/Algebra/Associated/Basic.lean

modified theorem Associates.mk_injective

modified theorem prime_dvd_prime_iff_eq

Modified Mathlib/Algebra/BigOperators/Associated.lean

modified theorem Finset.prod_primes_dvd

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

modified theorem exists_eq_pow_of_mul_eq_pow

Modified Mathlib/Algebra/Group/Units.lean

modified theorem isUnit_iff_eq_one

modified theorem units_eq_one

Modified Mathlib/Data/List/Prime.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

modified theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff

modified theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime