finrank_lt_of_rank_lt — Mathlib

English

If the rank of M is strictly less than n, then finrank_R M is strictly less than n.

Русский

Если ранг M строго меньше n, то finrank_R M строго меньше n.

LaTeX

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

Lean4

theorem finrank_lt_of_rank_lt {n : ℕ} (h : Module.rank R M < ↑n) : finrank R M < n :=
  by
  rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans (nat_lt_aleph0 n)
  · exact nat_lt_aleph0 n

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