∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B],
      (∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1