rTensorAlgHom_apply_eq — Mathlib

English

The map rTensorAlgHom is equal to the linear map rTensor when compared via the underlying linear map equality.

Русский

Для rTensorAlgHom совпадение с линейным отображением rTensor истинно через соответствие линейных отображений.

LaTeX

$$$rTensorAlgHom \\; \\text{as linear map} = rTensor$$$

Lean4

theorem rTensorAlgHom_apply_eq (p : MvPolynomial σ S ⊗[R] N) : rTensorAlgHom (S := S) p = rTensor p :=
  by
  rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
  rfl

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