Commit 2026-03-02 23:05 f10bf357

View on Github →

refactor(RingTheory/Localization/Integral): Simplify integerNormalization (#34877) This PR does the following:

  • Add two lemmas exists_integer_polynomial_multiple and exists_integer_polynomial_multiple_and_support_subset which are easy consequence of exists_integer_multiple and exists_support_eq_of_mem_lifts, using the Polynomial.isLocalization instance.
  • Simplify the definition of integerNormalization to directly choose an integer multiple using these lemmas, without having to construct its coefficients by hand.
  • As a consequence, deprecate coeffIntegerNormalization, coeffIntegerNormalization_of_coeff_zero, coeffIntegerNormalization_mem_support and integerNormalization_coeff which were only used in that construction.
  • Rename integerNormalization_map_to_map to integerNormalization_spec (also providing a deprecated alias) and make the statement include (integerNormalization M p).support ⊆ p.support.
  • Simplify the proofs of integerNormalization_spec and integerNormalization_eq_zero_iff using the new definition.

Estimated changes