Theorems · Theorem · commutative algebra
Subalgebra.LinearDisjoint.rank_sup_of_free
∀ {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.Free R ↥B], Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥BIn a commutative ring, if subalgebras A and B are linearly disjoint and they are
free modules, then the rank of A ⊔ B is equal to the product of the rank of A and B.
- Defined in
- Mathlib.RingTheory.LinearDisjoint
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- mul_oneproof · cited by 3,885
- Cardinalstatement and proof · cited by 2,598
- Nontrivialproof · cited by 2,416
- Subalgebrastatement and proof · cited by 1,353
- Module.Freestatement and proof · cited by 597
- Module.rankstatement and proof · cited by 496
- AlgEquiv.toLinearEquivproof · cited by 117
- Subalgebra.LinearDisjointstatement and proof · cited by 75
- LinearEquiv.rank_eqproof · cited by 31
- rank_subsingletonproof · cited by 19
Cited by2
Results whose statement or proof uses this declaration.
- IntermediateField.LinearDisjoint.rank_supproof · cited by 1
- Subalgebra.LinearDisjoint.finrank_sup_of_freeproof · cited by 0