eq_of_le_of_finrank_le — Mathlib

English

If F ≤ E are intermediate fields and finrank E ≤ finrank F with F finite over K, then F = E.

Русский

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

LaTeX

$$$ (F \le E) \land (finrank_K E \le finrank_K F) \Rightarrow F = E $$$

Lean4

/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
then `F = E`. -/
theorem eq_of_le_of_finrank_le [hfin : FiniteDimensional K E] (h_le : F ≤ E) (h_finrank : finrank K E ≤ finrank K F) :
    F = E :=
  haveI : Module.Finite K E.toSubalgebra := hfin
  toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank

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