Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.of_linearDisjoint_finite

∀ {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] [Algebra.IsIntegral R ↥B],
  (∀ (A' B' : Subalgebra R S), A' ≤ A → B' ≤ B → ∀ [Module.Finite R ↥A'] [Module.Finite R ↥B'], A'.LinearDisjoint B') →
    A.LinearDisjoint B

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.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.IsIntegralAlgebra.IsIntegral