tensorModelOfHasCoeffsEquiv_symm_tmul

English

The model homomorphisms respect the HasCoeffs structure and map functions accordingly.

Русский

Гомоморфизмы модели совместимы с HasCoeffs и отображают функции соответствующим образом.

LaTeX

$$$\\text{HasCoeffs}(P)\\Rightarrow\\text{compatibility}_{\\text{model}}(P)$$$

Lean4

@[simp]
theorem tensorModelOfHasCoeffsEquiv_symm_tmul (x : MvPolynomial ι R₀) :
    (P.tensorModelOfHasCoeffsEquiv R₀).symm (MvPolynomial.aeval P.val x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) :=
  tensorModelOfHasCoeffsInv_aeval_val _ x

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