liftBaseChange_one_tmul — Mathlib

English

On simple tensors, the lifted map coincides with the action of the first factor: (l.liftBaseChange A)(x ⊗ y) = x · l(y).

Русский

На простых тензоре l.liftBaseChange совпадает с действием первого множителя: (l.liftBaseChange A)(x ⊗ y) = x · l(y).

LaTeX

$$$(l.liftBaseChange A)(x \\otimes y) = x \\cdot l(y)$$$

Lean4

theorem liftBaseChange_one_tmul (l : M →ₗ[R] N) (y) : l.liftBaseChange A (1 ⊗ₜ y) = l y := by simp

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