tensorModelOfHasCoeffsInv_aeval_val

English

Equation relating algebra map and quotients via the inverse tensor model.

Русский

Уравнение, связывающее алгебраическое отображение и деление через обратную модель.

LaTeX

$$$P.tensorModelOfHasCoeffsInv R_0\\ (\\mathrm{MvPolynomial}.aeval P.val\\ x) = 1 \\otimes_{R_0} (\\mathrm{Ideal.Quotient.mk}\\ _ x)$$$

Lean4

@[simp]
theorem tensorModelOfHasCoeffsInv_aeval_val (x : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsInv R₀ (MvPolynomial.aeval P.val x) = 1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) :=
  by
  rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]
  simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]

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