English
Let M be a finite-dimensional module over a semiring R. If n ∈ ℕ satisfies n < finrank_R M, then the cardinal rank of M satisfies (n in ℕ, cast to a cardinal) (n : Card) < rank_R M.
Русский
Пусть M является конечномерным модулем над полем (кольцом) R. Для любого натурального числа n, если n < finrank_R M, то (n, превращённое в кардинал) меньше чем rank_R M.
LaTeX
$$$\\forall {R,M} [Semiring R] [AddCommMonoid M] [Module R M] \\; (n : \\mathbb{N}) \\, (n < \\mathrm{finrank}_R M) \Rightarrow (n : \\mathrm{Cardinal}) < \\mathrm{rank}_R M$$$
Lean4
theorem lt_rank_of_lt_finrank {n : ℕ} (h : n < finrank R M) : ↑n < Module.rank R M :=
by
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
· exact nat_lt_aleph0 n
· contrapose! h
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
exact n.zero_le
