Commit 2026-03-25 17:09 36653f09

View on Github →

feat(RingTheory/Localization/Integral): generalize IsFractionRing.integerNormalization_eq_zero_iff (#37003) We prove

IsLocalization.integerNormalization_eq_zero_iff {R S : Type *} [CommRing R] {M : Submonoid R} 
  [CommRing S] [Algebra R S] [IsLocalization M S] [IsDomain R] (hM : M ≤ nonZeroDivisors R) (p : S[X]) :
  integerNormalization M p = 0 ↔ p = 0

which generalizes the current IsFractionRing.integerNormalization_eq_zero_iff.

Estimated changes