Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left

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

If A and B are linearly disjoint, if A is free and B is flat, then [B[A] : B] = [A : R]. See also Subalgebra.adjoin_rank_le.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.FreeModule.FlatNontrivialNontrivial