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

@[deprecated MvPolynomial.map_frobenius_expand (since := "2025-12-27")]

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

Alias of MvPolynomial.map_frobenius_expand.

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

@[deprecated MvPolynomial.map_iterateFrobenius_expand (since := "2025-12-27")]

theorem MvPolynomial.map_expand_pow_char {σ : 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

Alias of MvPolynomial.map_iterateFrobenius_expand.