Commit 2023-08-10 12:07 8c698a52

feat: simple lemmas about polynomials and their degrees (#6220) This PR extracts some lemmas about polynomials that are helpful for the tactic compute_degree (#6221). The signature of a theorem changed:

theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`

Modified files:

Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf