includeRight_lid — Mathlib

English

The right identity map satisfies that m ⊗ r maps to r • m, i.e., the right unit acts by scalar multiplication.

Русский

Правый единичный элемент действует через скалярное умножение: (m ⊗ r) ↦ r • m.

LaTeX

$$$ (TensorProduct.rid R M) (m ⊗ r) = r \\cdot m $$$

Lean4

theorem includeRight_lid {S : Type*} [Semiring S] [Algebra R S] (m : R ⊗[R] M) :
    (1 : S) ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m :=
  by
  suffices
    ∀ m,
      (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap).comp (TensorProduct.lid R M).symm.toLinearMap m =
        1 ⊗ₜ[R] m
    by simp [← this]
  intros; simp

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