English
Let p be any family of mv polynomials as above. The inverse bijection applied to the coefficient function (i ↦ (p_i).coeff on the chosen index) returns precisely the original family together with the obvious containment data for the supports.
Русский
Пусть дана такая же семья mv-полиномов; обратная биекция, действующая на коэффициентную функцию, возвращает исходную семью вместе с очевидной информацией о включении поддержек.
LaTeX
$$$(\\mathrm{mvPolynomialSupportLEEquiv}\\, monoms)^{ -1} (\\lambda i. (p_i).\\mathrm{coeff}) = \\langle p, \\text{proofs} \\rangle$$$
Lean4
@[simp]
theorem MvPolynomialSupportLEEquiv_symm_apply_coeff [DecidableEq κ] [CommRing R] [DecidableEq R]
(p : ι → MvPolynomial κ R) :
(mvPolynomialSupportLEEquiv (fun i => (p i).support)).symm (fun i => (p i.1).coeff i.2.1) =
⟨p, fun _ => Finset.Subset.refl _⟩ :=
(mvPolynomialSupportLEEquiv (R := R) (fun i : ι => (p i).support)).symm_apply_apply ⟨p, fun _ => Finset.Subset.refl _⟩
