Theorems · Theorem · field theory
Subfield.relrank_mul_rank_top
∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A ≤ B → A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E- Defined in
- Mathlib.FieldTheory.Relrank
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebraproof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- IsScalarTowerproof · cited by 3,896
- Cardinalstatement and proof · cited by 2,598
- Module.rankstatement and proof · cited by 496
- RingHom.toAlgebraproof · cited by 337
- Subfieldstatement and proof · cited by 303
- IsScalarTower.of_algebraMap_eq'proof · cited by 101
- Subfield.relrankstatement · cited by 40
- rank_mul_rankproof · cited by 8
- Subfield.relrank_eq_rank_of_leproof · cited by 7
- Subfield.inclusionproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- IntermediateField.relrank_mul_rank_topproof · cited by 3
- Subfield.relfinrank_mul_finrank_topproof · cited by 1
- Subfield.relrank_dvd_rank_top_of_leproof · cited by 0