expand_expand — Mathlib

English

Expanding by p after expanding by q is the same as expanding by pq. For any f ∈ R[X],

Русский

Расширение по p после расширения по q равно расширению по pq. Для любого f ∈ R[X],

LaTeX

$$$\operatorname{expand}(R,p)\bigl(\operatorname{expand}(R,q) f\bigr) = \operatorname{expand}(R,pq) f$$$

Lean4

theorem expand_expand (f : R[X]) : expand R p (expand R q f) = expand R (p * q) f :=
  Polynomial.induction_on f (fun r => by simp_rw [expand_C]) (fun f g ihf ihg => by simp_rw [map_add, ihf, ihg])
    fun n r _ => by simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]

Похожие утверждения