Some results on dimensions of algebra adjoin

This file contains some results on dimensions of Algebra.adjoin.

theorem Subalgebra.rank_sup_le_of_free {R : Type u} {S : Type v} [CommRing R] [StrongRankCondition R] [CommRing S] [Algebra R S] (A B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B] : Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

If A and B are subalgebras of a commutative R-algebra S, both of them are free R-algebras, then the rank 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.

theorem Subalgebra.finrank_sup_le_of_free {R : Type u} {S : Type v} [CommRing R] [StrongRankCondition R] [CommRing S] [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.