English
If two families of polynomials f,g satisfy that bind₁ f(wittPolynomial(p, n)) = bind₁ g(wittPolynomial(p, n)) for all n, then f = g.
Русский
Если две families полиномов f,g удовлетворяют равенству bind₁ f(WittPolynomial(p,n)) = bind₁ g(WittPolynomial(p,n)) для всех n, то f = g.
LaTeX
$$$$\forall f,g:\mathbb{N}\to \mathrm{MvPolynomial}(\mathbb{N},\mathbb{Z}),\; (\forall n, \bind_1 f(\mathrm{wittPolynomial}(p, n)) = \bind_1 g(\mathrm{wittPolynomial}(p, n))) \Rightarrow f = g.$$$$
Lean4
theorem poly_eq_of_wittPolynomial_bind_eq' [Fact p.Prime] (f g : ℕ → MvPolynomial (idx × ℕ) ℤ)
(h : ∀ n, bind₁ f (wittPolynomial p _ n) = bind₁ g (wittPolynomial p _ n)) : f = g :=
by
ext1 n
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
rw [← funext_iff] at h
replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, bind₁_wittPolynomial_xInTermsOfW,
bind₁_X_right] using h
