toFunLinear_tmul_apply — Mathlib

English

For all a ∈ A and p ∈ R[X], the value of the linear map on the simple tensor a ⊗ p is exactly the bilinear map evaluated at (a, p).

Русский

Для любых a ∈ A и p ∈ R[X] значение линейного отображения на простом тензоре a ⊗ p равно значению биЛинейной карты на (a, p).

LaTeX

$$$toFunLinear_R A\\ (a \\otimes p) = toFunBilinear_R A\\ a\\ p$$$

Lean4

@[simp]
theorem toFunLinear_tmul_apply (a : A) (p : R[X]) : toFunLinear R A (a ⊗ₜ[R] p) = toFunBilinear R A a p :=
  rfl

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