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