relfinrank_dvd_finrank_top_of_le — Mathlib

English

If A ≤ B are intermediate F-subfields of E, then relfinrank A B divides finrank A E.

Русский

Если A ≤ B — промежуточные поля над F в E, то relfinrank A B делит finrank A E.

LaTeX

$$$ (A \le B) \Rightarrow \operatorname{relfinrank} A B \ \mid \ \operatorname{finrank} A E $$$

Lean4

theorem relfinrank_dvd_finrank_top_of_le (h : A ≤ B) : relfinrank A B ∣ finrank A E :=
  dvd_of_mul_right_eq _ (relfinrank_mul_finrank_top h)

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