relrank_dvd_rank_top_of_le — Mathlib

English

For any intermediate F-subfields A ⊆ E and B ⊆ E with A ≤ B, the index relrank A B divides the linear dimension of E over A.

Русский

Для любых промежуточных полей A ⊆ E и B ⊆ E с A ≤ B, индекс relrank A B делит размерность E над A.

LaTeX

$$$ (A \le B) \Rightarrow \operatorname{relrank} A B \ \mid \ \operatorname{Module.rank} A E $$$

Lean4

theorem relrank_dvd_rank_top_of_le (h : A ≤ B) : relrank A B ∣ Module.rank A E :=
  dvd_of_mul_right_eq _ (relrank_mul_rank_top h)

Похожие утверждения