English
For IsPoly₂ p f, the polynomial map in two arguments respects RingHom via map g in each argument.
Русский
Для IsPoly₂ p f полиномиальная карта в двух аргументах сохраняется через кольцевой гомоморфизм в каждом из аргументов.
LaTeX
$$$\text{IsPoly₂ } p f \rightarrow \forall g, x,y,\; map g (f x y) = f (map g x) (map g y).$$$
Lean4
theorem wittPolyProdRemainder_vars (n : ℕ) : (wittPolyProdRemainder p n).vars ⊆ univ ×ˢ range n :=
by
rw [wittPolyProdRemainder]
refine Subset.trans (vars_sum_subset _ _) ?_
rw [biUnion_subset]
intro x hx
apply Subset.trans (vars_mul _ _)
refine union_subset ?_ ?_
· apply Subset.trans (vars_pow _ _)
have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
rw [this, vars_C]
apply empty_subset
· apply Subset.trans (vars_pow _ _)
apply Subset.trans (wittMul_vars _ _)
apply product_subset_product (Subset.refl _)
simpa using hx
