Theorems · Theorem · field theory
IntermediateField.finrank_sup_le
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E1 E2 : IntermediateField K L), Module.finrank K ↥(E1 ⊔ E2) ≤ Module.finrank K ↥E1 * Module.finrank K ↥E2If E1 and E2 are intermediate fields, then the Module.finrank of
the compositum of E1 and E2 is less than or equal to the product of that of E1 and E2.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- LE.le.transproof · cited by 3,151
- le_reflproof · cited by 2,061
- FiniteDimensionalproof · cited by 1,854
- Module.finrankstatement and proof · cited by 1,770
- MulZeroClass.zero_mulproof · cited by 1,625
- Subalgebraproof · cited by 1,353
- IntermediateFieldstatement and proof · cited by 988
- Module.rankproof · cited by 496
- not_ltproof · cited by 306
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.