English
If B is integral over R and for every B' ⊆ B finitely generated, A is linearly disjoint from B', then A is linearly disjoint from B.
Русский
Если B интеграл над R и для каждого конечного B' ⊆ B выполняется, что A ⊥ B', тогда A ⊥ B.
LaTeX
$$$\\operatorname{IsIntegral}_R(B) \\land ( \\forall B'\\le B, [\\operatorname{Module.Finite}_R(B')] \\Rightarrow A \\mathrel{\\mathrm{LinearDisjoint}} B') \\Rightarrow A \\mathrel{\\mathrm{LinearDisjoint}} B.$$$
Lean4
/-- If `B/R` is integral, such that `A` and `B'` are linearly disjoint for all subalgebras `B'`
of `B` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint. -/
theorem of_linearDisjoint_finite_right [Algebra.IsIntegral R B]
(H : ∀ B' : Subalgebra R S, B' ≤ B → [Module.Finite R B'] → A.LinearDisjoint B') : A.LinearDisjoint B :=
(of_linearDisjoint_finite_left B A fun B' hB' _ ↦ (H B' hB').symm).symm
