small — Mathlib

English

If R is a small ring and S is an algebra of finite type over R, then S is small.

Русский

Если R малое кольцо и S — алгебра конечного типа над R, то S малое.

LaTeX

$$$Small(R) \Rightarrow Small(S) \text{ under } [Algebra\,FiniteType R S]$$$

Lean4

theorem small [Small.{u} R] [Algebra.FiniteType R S] : Small.{u} S :=
  by
  have : Small.{u} (⊤ : Subalgebra R S) := Subalgebra.FG.small Algebra.FiniteType.out
  rwa [← small_univ_iff]

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