Commit 2024-09-17 09:53 c479ef25

View on Github →

feat(Algebra/Ring/Subring/IntPolynomiall): add intPolynomial (#15733)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Subring/IntPolynomial.lean

added def Polynomial.int

added theorem Polynomial.int_coeff_eq

added theorem Polynomial.int_eval₂_eq

added theorem Polynomial.int_leadingCoeff_eq

added theorem Polynomial.int_monic_iff

added theorem Polynomial.int_natDegree