tensorModelOfHasCoeffsHom_tmul — Mathlib

English

The inverse of tensorModelOfHasCoeffsHom exists as an AlgHom from S to R ⊗_{R0} P.ModelOfHasCoeffs R0, under appropriate identifications.

Русский

Существование обратного элемента tensorModelOfHasCoeffsHom как AlgHom из S в R ⊗_{R0} P.ModelOfHasCoeffs R0 при соответствующих идентификациях.

LaTeX

$$$\\text{tensorModelOfHasCoeffsInv} : S \\to_{\\mathsf{Alg}} R \\otimes_{R_0} P.ModelOfHasCoeffs R_0$$$

Lean4

@[simp]
theorem tensorModelOfHasCoeffsHom_tmul (x : R) (y : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsHom R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
  rfl

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