fintypeBasisIndex — Mathlib

English

A module over a division ring is Noetherian if and only if its dimension (rank) is less than aleph-null.

Русский

Модуль над делением кольца является Noetherian тогда и только тогда, когда его размерность (ранг) меньше ℵ₀.

LaTeX

$$$$ IsNoetherian\\ K V \\iff \\operatorname{rank}_K V < \\aleph_0. $$$$

Lean4

/-- In a Noetherian module over a division ring, all bases are indexed by a finite type. -/
noncomputable def fintypeBasisIndex {ι : Type*} [IsNoetherian K V] (b : Basis ι K V) : Fintype ι :=
  b.fintypeIndexOfRankLtAleph0 (rank_lt_aleph0 K V)

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