comm_comp_includeRight — Mathlib

English

Composing the swap with the right inclusion equals the left inclusion: (comm R A B) ∘ includeRight = includeLeft.

Русский

Составление обмена с правой вставкой даёт левую вставку: comm R A B ∘ includeRight = includeLeft.

LaTeX

$$$ (\\mathrm{comm}_{R} A B) \\circ \\mathrm{includeRight} = \\mathrm{includeLeft} $$$

Lean4

@[simp]
theorem comm_comp_includeRight : (TensorProduct.comm R A B : A ⊗[R] B →ₐ[R] B ⊗[R] A).comp includeRight = includeLeft :=
  rfl

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