small — Mathlib

English

If a submodule P is finitely generated, then P is small (lives in a small universe).

Русский

Если подмодуль P конечнопорожден, то он малый (обладает малостью по вселенному рангу).

LaTeX

$$$\text{Small}(P)\quad\text{whenever } P \text{ is FG}$$$

Lean4

theorem small [Small.{u} R] (P : Submodule R M) (hP : P.FG) : Small.{u} P :=
  by
  rw [fg_iff_exists_fin_generating_family] at hP
  obtain ⟨n, s, rfl⟩ := hP
  rw [← Fintype.range_linearCombination]
  apply small_range

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