Theorem Associated.primeFactors_eq

Modification history

2024-10-17 19:04

Mathlib/RingTheory/Radical.lean

feat: UniqueFactorizationMonoid.factors_rel_of_associated (#17260)

Added Associated.primeFactors_eq View on Github →