Commit 2023-03-13 13:27 3e294a73

View on Github →

feat: Port/Data.Polynomial.IntegralNormalization (#2833)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/IntegralNormalization.lean

added theorem Polynomial.integralNormalization_aeval_eq_zero

added theorem Polynomial.integralNormalization_coeff

added theorem Polynomial.integralNormalization_coeff_degree

added theorem Polynomial.integralNormalization_coeff_natDegree

added theorem Polynomial.integralNormalization_coeff_ne_degree

added theorem Polynomial.integralNormalization_coeff_ne_natDegree

added theorem Polynomial.integralNormalization_eval₂_eq_zero

added theorem Polynomial.integralNormalization_support

added theorem Polynomial.integralNormalization_zero

added theorem Polynomial.monic_integralNormalization

added theorem Polynomial.support_integralNormalization