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.map_frobenius_expand {σ : 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_iterateFrobenius_expand {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : ℕ) [ExpChar R p] (f : MvPolynomial σ R) (n : ℕ) : (map (iterateFrobenius R p n)) ((expand (p ^ n)) f) = f ^ p ^ n

theorem FiniteField.MvPolynomial.expand_card {σ : Type u_1} {K : Type u_3} [Field K] [Fintype K] (f : MvPolynomial σ K) : (MvPolynomial.expand (Fintype.card K)) f = f ^ Fintype.card K