eq_of_le_of_finrank_eq — Mathlib

English

If F ≤ E and finrank F = finrank E (with E finite over K), then F = E.

Русский

Если F ≤ E и finrank F = finrank E (при этом E конечномерно над K), тогда F = E.

LaTeX

$$$ [FiniteDimensional K E] (F \le E) \land (finrank_K F = finrank_K E) \Rightarrow F = E $$$

Lean4

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

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