Theorems · Theorem · field theory
IntermediateField.rank_bot_mul_relrank
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
A ≤ B → Module.rank F ↥A * A.relrank B = Module.rank F ↥B- Defined in
- Mathlib.FieldTheory.Relrank
- Cited by
- 3 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.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- Cardinalstatement and proof · cited by 2,598
- IntermediateFieldstatement and proof · cited by 988
- Module.rankstatement and proof · cited by 496
- AlgHom.toRingHomproof · cited by 490
- RingHom.toAlgebraproof · cited by 337
- IntermediateField.relrankstatement · cited by 45
- IntermediateField.inclusionproof · cited by 32
- rank_mul_rankproof · cited by 8
- IntermediateField.relrank_eq_rank_of_leproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- IntermediateField.relrank_bot_leftproof · cited by 1
- IntermediateField.finrank_bot_mul_relfinrankproof · cited by 1
- IntermediateField.relrank_dvd_rank_botproof · cited by 0