tensorModelOfHasCoeffsEquiv — Mathlib

English

The evaluation map aeval composed with the relationOfHasCoeffs maps to zero in the quotient.

Русский

Оценка aeval после relationOfHasCoeffs отображает в ноль в фактор-модели.

LaTeX

$$$\\mathrm{MvPolynomial}.aeval\\ P.val\\ (\\mathrm{relationOfHasCoeffs}\\ R_0\\ r) = 0$$$

Lean4

/-- The natural isomorphism `R ⊗[R₀] S₀ ≃ₐ[R] S`. -/
noncomputable def tensorModelOfHasCoeffsEquiv : R ⊗[R₀] P.ModelOfHasCoeffs R₀ ≃ₐ[R] S :=
  AlgEquiv.ofAlgHom (P.tensorModelOfHasCoeffsHom R₀) (P.tensorModelOfHasCoeffsInv R₀) (P.hom_comp_inv R₀)
    (P.inv_comp_hom R₀)

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