rid_tmul — Mathlib

English

The symmetrized right identity inverse applied to m equals m ⊗ 1, i.e., the inverse of the right identity recovers the canonical tensor.

Русский

Обратное к правому идентификатору в симметризированной форме примененное к m даёт m ⊗ 1, т.е. восстанавливает канонический тензор.

LaTeX

$$$ (TensorProduct.rid R M).symm m = m \\otimes 1 $$$

Lean4

@[simp]
theorem rid_tmul (m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ r) = r • m :=
  rfl

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