Expand a polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ. #

Main definitions #

• Polynomial.expand R p f: expand the polynomial f with coefficients in a commutative semiring R by a factor of p, so expand R p (∑ aₙ xⁿ) is ∑ aₙ xⁿᵖ.
• Polynomial.contract p f: the opposite of expand, so it sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.
noncomputable def Polynomial.expand (R : Type u) [] (p : ) :

Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

Equations
Instances For
theorem Polynomial.coe_expand (R : Type u) [] (p : ) :
= Polynomial.eval₂ Polynomial.C (Polynomial.X ^ p)
theorem Polynomial.expand_eq_comp_X_pow {R : Type u} [] (p : ) {f : } :
f = f.comp (Polynomial.X ^ p)
theorem Polynomial.expand_eq_sum {R : Type u} [] (p : ) {f : } :
f = f.sum fun (e : ) (a : R) => Polynomial.C a * (Polynomial.X ^ p) ^ e
@[simp]
theorem Polynomial.expand_C {R : Type u} [] (p : ) (r : R) :
(Polynomial.C r) = Polynomial.C r
@[simp]
theorem Polynomial.expand_X {R : Type u} [] (p : ) :
Polynomial.X = Polynomial.X ^ p
@[simp]
theorem Polynomial.expand_monomial {R : Type u} [] (p : ) (q : ) (r : R) :
( r) = (Polynomial.monomial (q * p)) r
theorem Polynomial.expand_expand {R : Type u} [] (p : ) (q : ) (f : ) :
( f) = (Polynomial.expand R (p * q)) f
theorem Polynomial.expand_mul {R : Type u} [] (p : ) (q : ) (f : ) :
(Polynomial.expand R (p * q)) f = ( f)
@[simp]
theorem Polynomial.expand_zero {R : Type u} [] (f : ) :
f = Polynomial.C (Polynomial.eval 1 f)
@[simp]
theorem Polynomial.expand_one {R : Type u} [] (f : ) :
f = f
theorem Polynomial.expand_pow {R : Type u} [] (p : ) (q : ) (f : ) :
(Polynomial.expand R (p ^ q)) f = (⇑)^[q] f
theorem Polynomial.derivative_expand {R : Type u} [] (p : ) (f : ) :
Polynomial.derivative ( f) = (Polynomial.derivative f) * (p * Polynomial.X ^ (p - 1))
theorem Polynomial.coeff_expand {R : Type u} [] {p : } (hp : 0 < p) (f : ) (n : ) :
( f).coeff n = if p n then f.coeff (n / p) else 0
@[simp]
theorem Polynomial.coeff_expand_mul {R : Type u} [] {p : } (hp : 0 < p) (f : ) (n : ) :
( f).coeff (n * p) = f.coeff n
@[simp]
theorem Polynomial.coeff_expand_mul' {R : Type u} [] {p : } (hp : 0 < p) (f : ) (n : ) :
( f).coeff (p * n) = f.coeff n
theorem Polynomial.expand_injective {R : Type u} [] {n : } (hn : 0 < n) :

Expansion is injective.

theorem Polynomial.expand_inj {R : Type u} [] {p : } (hp : 0 < p) {f : } {g : } :
f = g f = g
theorem Polynomial.expand_eq_zero {R : Type u} [] {p : } (hp : 0 < p) {f : } :
f = 0 f = 0
theorem Polynomial.expand_ne_zero {R : Type u} [] {p : } (hp : 0 < p) {f : } :
f 0 f 0
theorem Polynomial.expand_eq_C {R : Type u} [] {p : } (hp : 0 < p) {f : } {r : R} :
f = Polynomial.C r f = Polynomial.C r
theorem Polynomial.natDegree_expand {R : Type u} [] (p : ) (f : ) :
( f).natDegree = f.natDegree * p
theorem Polynomial.leadingCoeff_expand {R : Type u} [] {p : } {f : } (hp : 0 < p) :
theorem Polynomial.monic_expand_iff {R : Type u} [] {p : } {f : } (hp : 0 < p) :
( f).Monic f.Monic
theorem Polynomial.Monic.expand {R : Type u} [] {p : } {f : } (hp : 0 < p) :
f.Monic( f).Monic

Alias of the reverse direction of Polynomial.monic_expand_iff.

theorem Polynomial.map_expand {R : Type u} [] {S : Type v} [] {p : } {f : R →+* S} {q : } :
@[simp]
theorem Polynomial.expand_eval {R : Type u} [] (p : ) (P : ) (r : R) :
@[simp]
theorem Polynomial.expand_aeval {R : Type u} [] {A : Type u_1} [] [Algebra R A] (p : ) (P : ) (r : A) :
( P) = (Polynomial.aeval (r ^ p)) P
noncomputable def Polynomial.contract {R : Type u} [] (p : ) (f : ) :

The opposite of expand: sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.

Equations
Instances For
theorem Polynomial.coeff_contract {R : Type u} [] {p : } (hp : p 0) (f : ) (n : ) :
.coeff n = f.coeff (n * p)
theorem Polynomial.map_contract {R : Type u} [] {S : Type v} [] {p : } (hp : p 0) {f : R →+* S} {q : } :
=
theorem Polynomial.contract_expand {R : Type u} [] (p : ) {f : } (hp : p 0) :
theorem Polynomial.contract_one {R : Type u} [] {f : } :
= f
theorem Polynomial.expand_contract {R : Type u} [] (p : ) [CharP R p] [] {f : } (hf : Polynomial.derivative f = 0) (hp : p 0) :
= f
theorem Polynomial.expand_contract' {R : Type u} [] (p : ) [ExpChar R p] [] {f : } (hf : Polynomial.derivative f = 0) :
= f
theorem Polynomial.expand_char {R : Type u} [] (p : ) [ExpChar R p] (f : ) :
Polynomial.map (frobenius R p) ( f) = f ^ p
theorem Polynomial.map_expand_pow_char {R : Type u} [] (p : ) [ExpChar R p] (f : ) (n : ) :
Polynomial.map ( ^ n) ((Polynomial.expand R (p ^ n)) f) = f ^ p ^ n
theorem Polynomial.rootMultiplicity_expand_pow {R : Type u} [] {p : } {n : } [ExpChar R p] {f : } {r : R} :
theorem Polynomial.isLocalRingHom_expand (R : Type u) [] [] {p : } (hp : 0 < p) :
theorem Polynomial.of_irreducible_expand {R : Type u} [] [] {p : } (hp : p 0) {f : } (hf : Irreducible ( f)) :
theorem Polynomial.of_irreducible_expand_pow {R : Type u} [] [] {p : } (hp : p 0) {f : } {n : } :
Irreducible ((Polynomial.expand R (p ^ n)) f)