Commit 2024-11-30 18:25 883af569

View on Github →

chore: remove normalizeScaleRoots (#6183) Zulip

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.support_C

added theorem Polynomial.support_C_subset

Modified Mathlib/Algebra/Polynomial/Coeff.lean

Modified Mathlib/RingTheory/Algebraic/Basic.lean

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

deleted theorem leadingCoeff_smul_normalizeScaleRoots

deleted theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow

deleted theorem normalizeScaleRoots_degree

deleted theorem normalizeScaleRoots_eval₂_leadingCoeff_mul

deleted theorem normalizeScaleRoots_monic

deleted theorem normalizeScaleRoots_support

Modified Mathlib/RingTheory/Localization/Integral.lean

modified theorem IsIntegralClosure.isFractionRing_of_finite_extension

modified theorem integralClosure.isFractionRing_of_finite_extension

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

added theorem Polynomial.integralNormalization_C

modified theorem Polynomial.integralNormalization_coeff

modified theorem Polynomial.integralNormalization_coeff_degree

added theorem Polynomial.integralNormalization_coeff_degree_ne

added theorem Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow

modified theorem Polynomial.integralNormalization_coeff_natDegree

deleted theorem Polynomial.integralNormalization_coeff_ne_degree

modified theorem Polynomial.integralNormalization_coeff_ne_natDegree

added theorem Polynomial.integralNormalization_degree

added theorem Polynomial.integralNormalization_eval₂_leadingCoeff_mul

added theorem Polynomial.integralNormalization_mul_C_leadingCoeff

deleted theorem Polynomial.integralNormalization_support

added theorem Polynomial.leadingCoeff_smul_integralNormalization

modified theorem Polynomial.monic_integralNormalization

added theorem Polynomial.support_integralNormalization_subset