linearDisjoint_iff — Mathlib

English

Two subalgebras A,B are linearly disjoint if and only if their underlying submodules are linearly disjoint.

Русский

Две подалгебры A,B линейно дизъюнктны тогда и только тогда, когда их соответствующие подмодули линейно дизъюнктны.

LaTeX

$$$A.LinearDisjoint B \iff (\operatorname{toSubmodule} A).LinearDisjoint (\operatorname{toSubmodule} B)$$$

Lean4

theorem linearDisjoint_iff : A.LinearDisjoint B ↔ (toSubmodule A).LinearDisjoint (toSubmodule B) :=
  Iff.rfl

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