∀ {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