Theorems · Theorem · commutative algebra

Subalgebra.finrank_sup_le_of_free

∀ {R : Type u} {S : Type v} [inst : CommRing R] [StrongRankCondition R] [inst_2 : CommRing S] [inst_3 : Algebra R S]
  (A B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B],
  Module.finrank R ↥(A ⊔ B) ≤ Module.finrank R ↥A * Module.finrank R ↥B

If A and B are subalgebras of a commutative R-algebra S, both of them are free R-algebras, then the Module.finrank of the rank of the subalgebra generated by A and B over R is less than or equal to the product of that of A and B.

Defined in

Mathlib.RingTheory.Adjoin.Dimension

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingStrongRankConditionCommRingAlgebraModule.FreeModule.Free