finrank_le_of_le_right — Mathlib

English

If F ≤ E are finite-dimensional, then finrank K F ≤ finrank K E.

Русский

Если F ≤ E конечномерны над K, то finrank_K F ≤ finrank_K E.

LaTeX

$$$ [FiniteDimensional K (F \!\!\text{subfield})] (F \le E) \Rightarrow \operatorname{finrank}_K F \le \operatorname{finrank}_K E $$$

Lean4

theorem finrank_le_of_le_right [FiniteDimensional K E] (h : F ≤ E) : finrank K F ≤ finrank K E :=
  Nat.le_of_dvd Module.finrank_pos (finrank_dvd_of_le_right h)

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