Theorem UniqueFactorizationMonoid.dvd_of_normalized_factor

Modification history

2025-09-06 21:16
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
chore(RingTheory/UniqueFactorizationDomain): deprecate `dvd_of_normalized_factor` (#28430)
Deleted UniqueFactorizationMonoid.dvd_of_normalized_factorView on Github →
2025-05-27 08:57
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
chore: tidy various files (#25212)
Modified UniqueFactorizationMonoid.dvd_of_normalized_factorView on Github →
2025-05-22 12:54
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
feat(UniqueFactorizationMonoid): a `MulEquiv` that commutes with `normalize` preserves `normalizedFactors` (#25080)
Added UniqueFactorizationMonoid.dvd_of_normalized_factorView on Github →