single_commute_single — Mathlib

English

If hm commutes m1 and m2 in M and hr commutes r1 and r2 in R, then the two single elements commute: single m1 r1 and single m2 r2 commute.

Русский

Если m1 и m2 коммутируют в M, а r1 и r2 коммутируют в R, то элементы single m1 r1 и single m2 r2 коммутируют между собой.

LaTeX

$$$\operatorname{Commute}(\operatorname{single}(m_1,r_1),\operatorname{single}(m_2,r_2))$ при условии $Commute(m_1,m_2)$ и $Commute(r_1,r_2)$$$

Lean4

@[to_additive (attr := simp) (dont_translate := R) single_commute_single]
theorem single_commute_single (hm : Commute m₁ m₂) (hr : Commute r₁ r₂) : Commute (single m₁ r₁) (single m₂ r₂) := by
  simp [Commute, SemiconjBy, hm.eq, hr.eq]

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