eq_of_le_of_finrank_le' — Mathlib

English

If F ≤ E are intermediate fields and E is finite over L, then finrank_E L divides finrank_F L; more precisely, finrank_E L is a divisor of finrank_F L with quotient finrank F E.

Русский

Если F ≤ E — промежуточные поля и E конечномерно над L, то finrank_E L делит finrank_F L (с частным finrank F E).

LaTeX

$$$ (F \le E) \Rightarrow \operatorname{finrank}_E L \mid \operatorname{finrank}_F L $$$

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_le' [FiniteDimensional F L] (h_le : F ≤ E) (h_finrank : finrank F L ≤ finrank E L) :
    F = E := by
  refine le_antisymm h_le (fun l hl ↦ ?_)
  rwa [← mem_extendScalars (le_refl F),
    eq_of_le_of_finrank_le'' ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank,
    mem_extendScalars]

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