comm_trans_rTensorOne — Mathlib

English

Equality that identifies mulMap with composition of lTensorOne and submodule maps (eq_1).

Русский

Согласование mulMap с композициями отображений (eq_1).

LaTeX

$$mulMap( N ) = N.subtype ∘ₗ N.lTensorOne.toLinearMap$$

Lean4

@[simp]
theorem comm_trans_rTensorOne : (TensorProduct.comm R _ _).trans M.rTensorOne = M.lTensorOne :=
  by
  refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun r m ↦ ?_
  obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
  replace h : algebraMap R _ x = r := Subtype.val_injective h
  rw [← h]; simp

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