comp_assoc — Mathlib

English

Composition of polynomials is associative: (φ ∘ ψ) ∘ χ = φ ∘ (ψ ∘ χ).

Русский

Композиция полиномов ассоциативна: (φ ∘ ψ) ∘ χ = φ ∘ (ψ ∘ χ).

LaTeX

$$$$(\\varphi \\circ \\psi) \\circ \\chi = \\varphi \\circ (\\psi \\circ \\chi)$$$$

Lean4

theorem comp_assoc {R : Type*} [CommSemiring R] (φ ψ χ : R[X]) : (φ.comp ψ).comp χ = φ.comp (ψ.comp χ) := by
  refine Polynomial.induction_on φ ?_ ?_ ?_ <;>
    · intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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