Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Algebra.IsIntegral R ↥A], (∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B) → A.LinearDisjoint B

If A/R is integral, such that A' and B are linearly disjoint for all subalgebras A' of A which are finitely generated R-modules, then A and B are linearly disjoint.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.IsIntegral