finite — Mathlib

English

Let M be a finite R-module. If f: ι → M is linearly independent over R, then ι is finite.

Русский

Пусть M — конечномерный модуль над кольцом R. Если f: ι → M линейно независимо по R, то ι является сколь угодно конечно.

LaTeX

$$$\text{Module.Finite } R M \;\Longrightarrow\; (\text{LinearIndependent } R f) \Rightarrow \ Finite\ ι$$$

Lean4

theorem finite [Module.Finite R M] {ι : Type*} {f : ι → M} (h : LinearIndependent R f) : Finite ι :=
  Cardinal.lt_aleph0_iff_finite.1 <| h.lt_aleph0_of_finite

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