Commit 2024-02-14 22:15 4fe12e02

View on Github →

chore(RingTheory/MvPolynomial/Homogeneous): misc lemmas on homogeneous polyomials (#10478)

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.C_mul_X

added theorem MvPolynomial.IsHomogeneous.C_mul

added theorem MvPolynomial.IsHomogeneous.aeval

added theorem MvPolynomial.IsHomogeneous.eval₂

added theorem MvPolynomial.IsHomogeneous.map

added theorem MvPolynomial.IsHomogeneous.pow

added theorem MvPolynomial.isHomogeneous_C_mul_X_pow

added theorem MvPolynomial.isHomogeneous_X_pow