# Some results on dimensions of algebra adjoin #

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

source
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`.

source
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`.