Commit 2026-07-08 15:11 2f352487

View on Github →

refactor(Algebra): weaken NormalizationMonoid (#34179) This PR replaces the two fields

  normUnit_mul : ∀ {a b}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
  normUnit_coe_units : ∀ u : αˣ, normUnit u = u⁻¹

in the definition of NormalizationMonoid by

  normUnit_one : normUnit 1 = 1
  normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * u) = u⁻¹ * normUnit a

and rename the old version to StrongNormalizationMonoid. The vast majority of API continue to hold under this weakened notion of NormalizationMonoid; only a handful requires the original notion. Every cancellative monoid with zero admits a weakened NormalizationMonoid structure, and every GCDMonoid admits a weakened NormalizedGCDMonoid structure. This allows us to generalize Polynomial.normalizedGcdMonoid to all GCDMonoids.

Estimated changes

modified theorem Associated.eq_of_normalized
added theorem Associates.out_mul'
modified theorem Associates.out_mul
added theorem coe_normalizeHom
deleted theorem gcd_mul_lcm
modified theorem gcd_mul_left
modified theorem gcd_mul_right
modified theorem lcm_mul_left
modified theorem lcm_mul_right
added theorem lcm_ne_zero_iff
added theorem normUnit_coe_units
deleted theorem normUnit_one
modified def normalize
added def normalizeHom
modified theorem normalize_coe_units
modified theorem normalize_eq_normalize
modified theorem normalize_eq_normalize_iff
modified theorem normalize_eq_one
added theorem normalize_mul
modified theorem normalize_one
modified theorem normalize_zero
modified theorem Multiset.gcd_map_mul
modified theorem Polynomial.X_eq_normalize
modified theorem Polynomial.normUnit_X
modified theorem Polynomial.content_C_mul
modified theorem Polynomial.content_mul
modified theorem Polynomial.primPart_mul