small — Mathlib

English

If M is a finitely generated module over a small ring R, then M itself is small.

Русский

Если M является конечнопорожденным модулем над маленьким кольцом R, то сам M мал по universам.

LaTeX

$$$Small(R) \implies Small(M)$ under [Module.Finite R M]$$

Lean4

theorem _root_.Module.Finite.small [Small.{u} R] [Module.Finite R M] : Small.{u} M :=
  by
  have : Small.{u} (⊤ : Submodule R M) := FG.small _ (Module.finite_def.mp inferInstance)
  rwa [← small_univ_iff]

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