relrank_dvd_rank_bot — Mathlib

English

For any intermediate fields A ⊆ E and B ⊆ E, relrank A B divides the dimension of B over F.

Русский

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

LaTeX

$$$ \text{(no condition)} \quad \operatorname{relrank} A B \ \mid \ \operatorname{Module.rank} F B $$$

Lean4

theorem relrank_dvd_rank_bot : relrank A B ∣ Module.rank F B :=
  inf_relrank_right A B ▸ dvd_of_mul_left_eq _ (rank_bot_mul_relrank inf_le_right)

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