Results on MvPolynomial.expand

In this file we prove results about MvPolynomial.expand that require more than the basic API available in Mathlib.Algebra.*.

theorem MvPolynomial.expand_char {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : ℕ) [ExpChar R p] {f : MvPolynomial σ R} : (map (frobenius R p)) ((expand p) f) = f ^ p

theorem MvPolynomial.map_expand_char_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : ℕ) [ExpChar R p] (f : MvPolynomial σ R) (n : ℕ) : (map (frobenius R p ^ n)) ((expand (p ^ n)) f) = f ^ p ^ n