whiskerLeft_apply — Mathlib

English

The left whiskering map applied to a simple tensor gives the expected result: (L ◁ f)(l ⊗ m) = l ⊗ f m.

Русский

Левое усечение применено к простому тензору даёт ожидаемый результат: (L ◁ f)(l ⊗ m) = l ⊗ f(m).

LaTeX

$$$ (L \\triangleleft f)(l \\otimes m) = l \\otimes f(m) $$$

Lean4

@[simp]
theorem whiskerLeft_apply (L : ModuleCat.{u} R) {M N : ModuleCat.{u} R} (f : M ⟶ N) (l : L) (m : M) :
    (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
  rfl

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