Theorem normalize_eq_normalize_iff_associated

Modification history

2025-05-22 12:54

Mathlib/Algebra/GCDMonoid/Basic.lean

feat(UniqueFactorizationMonoid): a `MulEquiv` that commutes with `normalize` preserves `normalizedFactors` (#25080)

Added normalize_eq_normalize_iff_associated View on Github →