of_le_of_flat_right — Mathlib

English

If A and B are linearly disjoint and A', B' lie inside A,B with flatness assumptions, then A' and B' are linearly disjoint.

Русский

Если A и B линейно раздельны, и A', B' лежат внутри A,B с условиями плоскости, то A' и B' линейно раздельны.

LaTeX

$$$A \\perp_L B \\Rightarrow A' \\le A \\land B' \\le B \\land \\mathbf{Flat}_R(A) \\land \\mathbf{Flat}_R(B') \\Rightarrow A' \\perp_L B'$$$

Lean4

theorem of_le_of_flat_right {A' B' : Subalgebra R S} (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R B] [Module.Flat R A'] :
    A'.LinearDisjoint B' :=
  (H.of_le_left_of_flat ha).of_le_right_of_flat hb

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