Theorem Associated.normalizedFactors_eq

Modification history

2024-11-20 11:43

Mathlib/RingTheory/UniqueFactorizationDomain.lean

chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …

Modified Associated.normalizedFactors_eq View on Github →

2024-10-17 19:04

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat: UniqueFactorizationMonoid.factors_rel_of_associated (#17260)

Added Associated.normalizedFactors_eq View on Github →