Theorems · Theorem · field theory
Subfield.relrank_eq_rank_of_le
∀ {E : Type v} [inst : Field E] {A B : Subfield E} (h : A ≤ B), A.relrank B = Module.rank ↥A ↥(Subfield.extendScalars h)If A ≤ B, then Subfield.relrank A B is [B : A].
- Defined in
- Mathlib.FieldTheory.Relrank
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 86 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.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Moduleproof · cited by 20,661
- Semiringproof · cited by 13,802
- AddCommMonoidproof · cited by 12,281
- Algebraproof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- IsScalarTowerproof · cited by 3,896
- Cardinalstatement and proof · cited by 2,598
- SetLikeproof · cited by 1,084
- DivisionRingproof · cited by 1,062
- IntermediateFieldstatement and proof · cited by 988
- Module.rankstatement and proof · cited by 496
- Semifieldproof · cited by 439
Cited by7
Results whose statement or proof uses this declaration.
- Subfield.inf_relrank_rightproof · cited by 3
- Subfield.relrank_mul_rank_topproof · cited by 3
- Subfield.relrank_mul_relrankproof · cited by 3
- IntermediateField.relrank_eq_rank_of_leproof · cited by 3
- Subfield.relrank_selfproof · cited by 2
- Subfield.relrank_top_rightproof · cited by 2
- Subfield.relfinrank_eq_finrank_of_leproof · cited by 0