pUnitAlgEquiv_symm_monomial — Mathlib

English

Under the canonical isomorphism between MV-polynomials in one variable and polynomials over R, the image of a mv-monomial monomial d r is exactly the univariate polynomial monomial with index d() and coefficient r.

Русский

При каноническом изоморфизме между MV-многочленами в одной переменной и многочленами над R образ mv-мономиала monomial d r — это точно одночлен полиномов по переменной, индексируемый d(), с коэффициентом r.

LaTeX

$$$$ \\text{pUnitAlgEquiv}_R(\\text{monomial}(d,r)) = \\text{Polynomial.monomial}(d(), r). $$$$

Lean4

theorem pUnitAlgEquiv_symm_monomial {d : PUnit →₀ ℕ} {r : R} :
    (MvPolynomial.pUnitAlgEquiv R).symm (Polynomial.monomial (d ()) r) = MvPolynomial.monomial d r := by
  simp [MvPolynomial.monomial_eq]

Похожие утверждения