English
init respects integer scalar multiplication: init_n(m • x) = m • init_n(x).
Русский
init сохраняет целочисленное скалярное умножение: init_n(m • x) = m • init_n(x).
LaTeX
$$$$\operatorname{init}_n(m \cdot x) = m \cdot \operatorname{init}_n x.$$$$
Lean4
/-- The composition of polynomial functions is polynomial. -/
instance comp {h f g} [hh : IsPoly₂ p h] [hf : IsPoly p f] [hg : IsPoly p g] :
IsPoly₂ p fun _ _Rcr x y => h (f x) (g y) := by
obtain ⟨φ, hf⟩ := hf
obtain ⟨ψ, hg⟩ := hg
obtain ⟨χ, hh⟩ := hh
refine
⟨⟨fun n ↦
bind₁ (uncurry <| ![fun k ↦ rename (Prod.mk (0 : Fin 2)) (φ k), fun k ↦ rename (Prod.mk (1 : Fin 2)) (ψ k)])
(χ n),
?_⟩⟩
intros
funext n
simp +unfoldPartialApp only [peval, aeval_bind₁, hh, hf, hg, uncurry]
apply eval₂Hom_congr rfl _ rfl
ext ⟨i, n⟩
fin_cases i <;> simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]
