tensorKaehlerEquiv_tmul — Mathlib

English

The action on simple tensors is given by tensorKaehlerEquiv(R,S,A,B)(a ⊗ b) = a • map_{R,S,A,B}(b).

Русский

Действие на простых тензорных произведениях задаётся как tensorKaehlerEquiv(...)(a ⊗ b) = a • map(b).

LaTeX

$$$\\mathrm{tensorKaehlerEquiv}(R,S,A,B)(a \\otimes b) = a \\cdot \\mathrm{map}(R,S,A,B)(b)$$$

Lean4

@[simp]
theorem tensorKaehlerEquiv_tmul [Algebra.IsPushout R S A B] (a b) :
    tensorKaehlerEquiv R S A B (a ⊗ₜ b) = a • map R S A B b :=
  LinearMap.liftBaseChange_tmul _ _ _ _

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