# mathlib3documentation

data.polynomial.expand

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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
theorem polynomial.coe_expand (R : Type u) (p : ) :
theorem polynomial.expand_eq_sum {R : Type u} (p : ) {f : polynomial R} :
p) f = f.sum (λ (e : ) (a : R), * ^ e)
@[simp]
theorem polynomial.expand_C {R : Type u} (p : ) (r : R) :
p) =
@[simp]
theorem polynomial.expand_X {R : Type u} (p : ) :
@[simp]
theorem polynomial.expand_monomial {R : Type u} (p q : ) (r : R) :
p) ( r) = (polynomial.monomial (q * p)) r
theorem polynomial.expand_expand {R : Type u} (p q : ) (f : polynomial R) :
p) ( q) f) = (p * q)) f
theorem polynomial.expand_mul {R : Type u} (p q : ) (f : polynomial R) :
(p * q)) f = p) ( q) f)
@[simp]
theorem polynomial.expand_zero {R : Type u} (f : polynomial R) :
0) f =
@[simp]
theorem polynomial.expand_one {R : Type u} (f : polynomial R) :
1) f = f
theorem polynomial.expand_pow {R : Type u} (p q : ) (f : polynomial R) :
(p ^ q)) f = p)^[q] f
theorem polynomial.derivative_expand {R : Type u} (p : ) (f : polynomial R) :
theorem polynomial.coeff_expand {R : Type u} {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
( p) f).coeff n = ite (p n) (f.coeff (n / p)) 0
@[simp]
theorem polynomial.coeff_expand_mul {R : Type u} {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
( p) f).coeff (n * p) = f.coeff n
@[simp]
theorem polynomial.coeff_expand_mul' {R : Type u} {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
( p) 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 : polynomial R} :
p) f = p) g f = g
theorem polynomial.expand_eq_zero {R : Type u} {p : } (hp : 0 < p) {f : polynomial R} :
p) f = 0 f = 0
theorem polynomial.expand_ne_zero {R : Type u} {p : } (hp : 0 < p) {f : polynomial R} :
p) f 0 f 0
theorem polynomial.expand_eq_C {R : Type u} {p : } (hp : 0 < p) {f : polynomial R} {r : R} :
p) f =
theorem polynomial.nat_degree_expand {R : Type u} (p : ) (f : polynomial R) :
theorem polynomial.monic.expand {R : Type u} {p : } {f : polynomial R} (hp : 0 < p) (h : f.monic) :
( p) f).monic
theorem polynomial.map_expand {R : Type u} {S : Type v} {p : } {f : R →+* S} {q : polynomial R} :
( p) q) = p) q)
@[simp]
theorem polynomial.expand_eval {R : Type u} (p : ) (P : polynomial R) (r : R) :
( p) P) = polynomial.eval (r ^ p) P
@[simp]
theorem polynomial.expand_aeval {R : Type u} {A : Type u_1} [semiring A] [ A] (p : ) (P : polynomial R) (r : A) :
( p) P) = (polynomial.aeval (r ^ p)) P
noncomputable def polynomial.contract {R : Type u} (p : ) (f : polynomial R) :

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

Equations
theorem polynomial.coeff_contract {R : Type u} {p : } (hp : p 0) (f : polynomial R) (n : ) :
f).coeff n = f.coeff (n * p)
theorem polynomial.contract_expand {R : Type u} (p : ) {f : polynomial R} (hp : p 0) :
( p) f) = f
theorem polynomial.expand_contract {R : Type u} (p : ) [ p] {f : polynomial R} (hf : = 0) (hp : p 0) :
p) f) = f
theorem polynomial.expand_char {R : Type u} (p : ) [ p] [hp : fact (nat.prime p)] (f : polynomial R) :
polynomial.map p) ( p) f) = f ^ p
theorem polynomial.map_expand_pow_char {R : Type u} (p : ) [ p] [hp : fact (nat.prime p)] (f : polynomial R) (n : ) :
polynomial.map p ^ n) ( (p ^ n)) f) = f ^ p ^ n
theorem polynomial.is_local_ring_hom_expand (R : Type u) [comm_ring R] [is_domain R] {p : } (hp : 0 < p) :
theorem polynomial.of_irreducible_expand {R : Type u} [comm_ring R] [is_domain R] {p : } (hp : p 0) {f : polynomial R} (hf : irreducible ( p) f)) :
theorem polynomial.of_irreducible_expand_pow {R : Type u} [comm_ring R] [is_domain R] {p : } (hp : p 0) {f : polynomial R} {n : } :
irreducible ( (p ^ n)) f)