symm_of_commute — Mathlib

English

If A and B are linearly disjoint and every element of A commutes with every element of B, then B is linearly disjoint from A.

Русский

Если A и B линейно дизъюнктны и все элементы A коммутируют с элементами B, то B линейно дизъюнктна по отношению к A.

LaTeX

$$$A.LinearDisjoint B \Rightarrow B.LinearDisjoint A \quad \text{(under commuting condition).}$$$

Lean4

/-- Linear disjointness is symmetric if elements in the module commute. -/
theorem symm_of_commute (H : A.LinearDisjoint B) (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : B.LinearDisjoint A :=
  Submodule.LinearDisjoint.symm_of_commute H hc

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