English
The composition of a polynomial function with a binary polynomial function is polynomial: if h,g,f are polynomial with respect to p, then h(f(x), g(y)) is polynomial.
Русский
Композиция полиномной функции с двоичной полиномной функцией есть полином: если h, f, g — полиномы по p, то h(f(x), g(y)) — полином.
LaTeX
$$$$IsPoly_2(p,\, h) \land IsPoly(p, f) \land IsPoly(p, g) \Rightarrow IsPoly_2(p, \lambda x y. h (f x) (g y)).$$$$
Lean4
/-- The diagonal `fun x ↦ f x x` of a polynomial function `f` is polynomial. -/
instance diag {f} [hf : IsPoly₂ p f] : IsPoly p fun _ _Rcr x => f x x :=
by
obtain ⟨φ, hf⟩ := hf
refine ⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ n), ?_⟩⟩
intros; funext n
simp +unfoldPartialApp only [hf, peval, uncurry, aeval_bind₁]
apply eval₂Hom_congr rfl _ rfl
ext ⟨i, k⟩
fin_cases i <;> simp
