linearDisjoint_comm_of_commute — Mathlib

English

The disjointness relation between A and B is symmetric if elements commute: A.LinearDisjoint B ↔ B.LinearDisjoint A when a ∈ A and b ∈ B commute.

Русский

Связь дизъюнктности между A и B симметрична при условии коммутатирования элементов: A.LinearDisjoint B ↔ B.LinearDisjoint A, если a и b commute.

LaTeX

$$$A.LinearDisjoint B \iff B.LinearDisjoint A$ (при коммутировании элементов).$$

Lean4

/-- Linear disjointness is symmetric if elements in the module commute. -/
theorem linearDisjoint_comm_of_commute (hc : ∀ (a : A) (b : B), Commute a.1 b.1) :
    A.LinearDisjoint B ↔ B.LinearDisjoint A :=
  ⟨fun H ↦ H.symm_of_commute hc, fun H ↦ H.symm_of_commute fun _ _ ↦ (hc _ _).symm⟩

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