finrank_le_of_le_left — Mathlib

English

If F ≤ E are finite-dimensional, then finrank_E L ≤ finrank_F L.

Русский

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

LaTeX

$$$ [FiniteDimensional (Subtype \{x\;|\; x \in F\}) L] \Rightarrow \operatorname{finrank}_E L \le \operatorname{finrank}_F L $$$

Lean4

theorem finrank_le_of_le_left [FiniteDimensional F L] (h : F ≤ E) : finrank E L ≤ finrank F L :=
  Nat.le_of_dvd Module.finrank_pos (finrank_dvd_of_le_left h)

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