finrank_dvd_of_le_right — Mathlib

English

If F ≤ E are intermediate fields, then finrank K F x divides finrank K E x (in terms of subfield ranks).

Русский

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

LaTeX

$$$ (F \le E) \Rightarrow \operatorname{finrank}_K(\text{F-sub}) \mid \operatorname{finrank}_K(\text{E-sub}) $$$

Lean4

theorem finrank_dvd_of_le_right (h : F ≤ E) : finrank K F ∣ finrank K E :=
  by
  let _ := (inclusion h).toRingHom.toAlgebra
  exact Dvd.intro (finrank F E) (finrank_mul_finrank K F E)

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