inf_eq_bot_of_commute — Mathlib

English

If A and B are linearly disjoint and every pair of elements from A ∩ B commute, then A ∩ B = {0}.

Русский

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

LaTeX

$$$A \\cap B = \\{0\\}$$$

Lean4

theorem inf_eq_bot_of_commute (H : A.LinearDisjoint B) (hc : ∀ (a b : ↥(A ⊓ B)), Commute a.1 b.1) : A ⊓ B = ⊥ :=
  eq_bot_of_rank_le_one (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left H hc)

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