Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.of_finrank_coprime_of_free

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Module.Free R ↥A] [Module.Free R ↥B] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)]
  [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)], (Module.finrank R ↥A).Coprime (Module.finrank R ↥B) → A.LinearDisjoint B

If the rank of A and B are coprime, and they satisfy some freeness condition, then A and B are linearly disjoint.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.FreeModule.FreeModule.FreeModule.Free