English
If A and B are integral over R, and every finite pair of subalgebras is linearly disjoint, then A and B are linearly disjoint.
Русский
Если A и B интегральны над R, и любая пара конечных подалгебр линейно диссоциирована, тогда A и B линейно несвязаны.
LaTeX
$$$\\text{IsIntegral}_R(A) \\land \\text{IsIntegral}_R(B) \\land \\forall (A',B'), A' \\le A \\land B' \\le B \\rightarrow [\\operatorname{Module.Finite}_R(A')] \\rightarrow [\\operatorname{Module.Finite}_R(B')] \\rightarrow A'\\mathrel{\\mathrm{LinearDisjoint}} B' \\Rightarrow A\\mathrel{\\mathrm{LinearDisjoint}} B.$$$
Lean4
/-- If `A/R` and `B/R` are integral, such that any finite subalgebras in `A` and `B` are
linearly disjoint, then `A` and `B` are linearly disjoint. -/
theorem of_linearDisjoint_finite [Algebra.IsIntegral R A] [Algebra.IsIntegral R B]
(H :
∀ (A' B' : Subalgebra R S),
A' ≤ A → B' ≤ B → [Module.Finite R A'] → [Module.Finite R B'] → A'.LinearDisjoint B') :
A.LinearDisjoint B :=
of_linearDisjoint_finite_left A B fun _ hA' _ ↦ of_linearDisjoint_finite_right _ B fun _ hB' _ ↦ H _ _ hA' hB'
