mathlib documentation

data.polynomial.expand

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

Main definitions #

noncomputable def polynomial.expand (R : Type u) [comm_semiring R] (p : ) :

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

Equations
theorem polynomial.expand_eq_sum {R : Type u} [comm_semiring R] (p : ) {f : polynomial R} :
(polynomial.expand R p) f = f.sum (λ (e : ) (a : R), polynomial.C a * (polynomial.X ^ p) ^ e)
@[simp]
theorem polynomial.expand_C {R : Type u} [comm_semiring R] (p : ) (r : R) :
@[simp]
@[simp]
theorem polynomial.expand_monomial {R : Type u} [comm_semiring R] (p q : ) (r : R) :
theorem polynomial.expand_expand {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :
theorem polynomial.expand_mul {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :
@[simp]
theorem polynomial.expand_one {R : Type u} [comm_semiring R] (f : polynomial R) :
theorem polynomial.expand_pow {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :
theorem polynomial.coeff_expand {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff n = ite (p n) (f.coeff (n / p)) 0
@[simp]
theorem polynomial.coeff_expand_mul {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff (n * p) = f.coeff n
@[simp]
theorem polynomial.coeff_expand_mul' {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff (p * n) = f.coeff n
theorem polynomial.expand_inj {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f g : polynomial R} :
theorem polynomial.expand_eq_zero {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f : polynomial R} :
(polynomial.expand R p) f = 0 f = 0
theorem polynomial.expand_ne_zero {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f : polynomial R} :
theorem polynomial.expand_eq_C {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f : polynomial R} {r : R} :
theorem polynomial.monic.expand {R : Type u} [comm_semiring R] {p : } {f : polynomial R} (hp : 0 < p) (h : f.monic) :
theorem polynomial.map_expand {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] {p : } {f : R →+* S} {q : polynomial R} :
theorem polynomial.expand_injective {R : Type u} [comm_semiring R] {n : } (hn : 0 < n) :

Expansion is injective.

@[simp]
theorem polynomial.expand_eval {R : Type u} [comm_semiring R] (p : ) (P : polynomial R) (r : R) :
@[simp]
theorem polynomial.expand_aeval {R : Type u} [comm_semiring R] {A : Type u_1} [semiring A] [algebra R A] (p : ) (P : polynomial R) (r : A) :
noncomputable def polynomial.contract {R : Type u} [comm_semiring R] (p : ) (f : polynomial R) :

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

Equations
theorem polynomial.coeff_contract {R : Type u} [comm_semiring R] {p : } (hp : p 0) (f : polynomial R) (n : ) :
theorem polynomial.contract_expand {R : Type u} [comm_semiring R] (p : ) {f : polynomial R} (hp : p 0) :
theorem polynomial.expand_contract {R : Type u} [comm_semiring R] (p : ) [char_p R p] [no_zero_divisors R] {f : polynomial R} (hf : polynomial.derivative f = 0) (hp : p 0) :
theorem polynomial.expand_char {R : Type u} [comm_semiring R] (p : ) [char_p R p] [hp : fact (nat.prime p)] (f : polynomial R) :
theorem polynomial.map_expand_pow_char {R : Type u} [comm_semiring R] (p : ) [char_p R p] [hp : fact (nat.prime p)] (f : polynomial R) (n : ) :
polynomial.map (frobenius R p ^ n) ((polynomial.expand R (p ^ n)) f) = f ^ p ^ n
theorem polynomial.of_irreducible_expand {R : Type u} [comm_ring R] [is_domain R] {p : } (hp : p 0) {f : polynomial R} (hf : irreducible ((polynomial.expand R 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 : } :