eq_of_le_of_finrank_eq' — Mathlib

English

If F ≤ E are intermediate fields, then finrank K F x equals finrank K E x, expressed via the respective submodule ranks, with F ≤ E.

Русский

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

LaTeX

$$$ (F \le E) \Rightarrow \operatorname{finrank}_K(\operatorname{Subfield}(F)) \;\big|\; \operatorname{finrank}_K(\operatorname{Subfield}(E)) $$$

Lean4

/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
then `F = E`. -/
theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E) (h_finrank : finrank F L = finrank E L) :
    F = E :=
  eq_of_le_of_finrank_le' h_le h_finrank.le

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