Documentation

Mathlib.Algebra.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) [CommSemiring R] (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) [CommSemiring R] (p : ) :
    (Polynomial.expand R p) = Polynomial.eval₂ Polynomial.C (Polynomial.X ^ p)
    theorem Polynomial.expand_eq_comp_X_pow {R : Type u} [CommSemiring R] (p : ) {f : Polynomial R} :
    (Polynomial.expand R p) f = f.comp (Polynomial.X ^ p)
    theorem Polynomial.expand_eq_sum {R : Type u} [CommSemiring R] (p : ) {f : Polynomial R} :
    (Polynomial.expand R p) f = f.sum fun (e : ) (a : R) => Polynomial.C a * (Polynomial.X ^ p) ^ e
    @[simp]
    theorem Polynomial.expand_C {R : Type u} [CommSemiring R] (p : ) (r : R) :
    (Polynomial.expand R p) (Polynomial.C r) = Polynomial.C r
    @[simp]
    theorem Polynomial.expand_X {R : Type u} [CommSemiring R] (p : ) :
    (Polynomial.expand R p) Polynomial.X = Polynomial.X ^ p
    @[simp]
    theorem Polynomial.expand_monomial {R : Type u} [CommSemiring R] (p : ) (q : ) (r : R) :
    theorem Polynomial.expand_expand {R : Type u} [CommSemiring R] (p : ) (q : ) (f : Polynomial R) :
    theorem Polynomial.expand_mul {R : Type u} [CommSemiring R] (p : ) (q : ) (f : Polynomial R) :
    @[simp]
    theorem Polynomial.expand_zero {R : Type u} [CommSemiring R] (f : Polynomial R) :
    (Polynomial.expand R 0) f = Polynomial.C (Polynomial.eval 1 f)
    @[simp]
    theorem Polynomial.expand_one {R : Type u} [CommSemiring R] (f : Polynomial R) :
    theorem Polynomial.expand_pow {R : Type u} [CommSemiring R] (p : ) (q : ) (f : Polynomial R) :
    (Polynomial.expand R (p ^ q)) f = ((Polynomial.expand R p))^[q] f
    theorem Polynomial.derivative_expand {R : Type u} [CommSemiring R] (p : ) (f : Polynomial R) :
    Polynomial.derivative ((Polynomial.expand R p) f) = (Polynomial.expand R p) (Polynomial.derivative f) * (p * Polynomial.X ^ (p - 1))
    theorem Polynomial.coeff_expand {R : Type u} [CommSemiring R] {p : } (hp : 0 < p) (f : Polynomial R) (n : ) :
    ((Polynomial.expand R p) f).coeff n = if p n then f.coeff (n / p) else 0
    @[simp]
    theorem Polynomial.coeff_expand_mul {R : Type u} [CommSemiring 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} [CommSemiring R] {p : } (hp : 0 < p) (f : Polynomial R) (n : ) :
    ((Polynomial.expand R p) f).coeff (p * n) = f.coeff n

    Expansion is injective.

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

    Alias of the reverse direction of Polynomial.monic_expand_iff.

    @[simp]
    theorem Polynomial.expand_eval {R : Type u} [CommSemiring R] (p : ) (P : Polynomial R) (r : R) :
    @[simp]
    theorem Polynomial.expand_aeval {R : Type u} [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] (p : ) (P : Polynomial R) (r : A) :
    noncomputable def Polynomial.contract {R : Type u} [CommSemiring R] (p : ) (f : Polynomial R) :

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

    Equations
    Instances For
      theorem Polynomial.coeff_contract {R : Type u} [CommSemiring R] {p : } (hp : p 0) (f : Polynomial R) (n : ) :
      (Polynomial.contract p f).coeff n = f.coeff (n * p)
      theorem Polynomial.contract_expand {R : Type u} [CommSemiring R] (p : ) {f : Polynomial R} (hp : p 0) :
      theorem Polynomial.expand_contract {R : Type u} [CommSemiring R] (p : ) [CharP R p] [NoZeroDivisors R] {f : Polynomial R} (hf : Polynomial.derivative f = 0) (hp : p 0) :
      theorem Polynomial.expand_contract' {R : Type u} [CommSemiring R] (p : ) [ExpChar R p] [NoZeroDivisors R] {f : Polynomial R} (hf : Polynomial.derivative f = 0) :
      theorem Polynomial.expand_char {R : Type u} [CommSemiring R] (p : ) [ExpChar R p] (f : Polynomial R) :
      theorem Polynomial.map_expand_pow_char {R : Type u} [CommSemiring R] (p : ) [ExpChar R 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} [CommRing R] [IsDomain R] {p : } (hp : p 0) {f : Polynomial R} (hf : Irreducible ((Polynomial.expand R p) f)) :
      theorem Polynomial.of_irreducible_expand_pow {R : Type u} [CommRing R] [IsDomain R] {p : } (hp : p 0) {f : Polynomial R} {n : } :