finrank_le_of_rank_le — Mathlib

English

If the rank of M is at most n, then finrank R M is at most n.

Русский

Если ранг M не превосходит n, то finrank_R M ≤ n.

LaTeX

$$$$\\operatorname{rank}_R M \\le n \\\\Rightarrow \\\\operatorname{finrank}_R M \\le n.$$$$

Lean4

theorem finrank_le_of_rank_le {n : ℕ} (h : Module.rank R M ≤ ↑n) : finrank R M ≤ n :=
  by
  rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans_lt (nat_lt_aleph0 n)
  · exact nat_lt_aleph0 n

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