Finite — Mathlib

English

A ring homomorphism f: A → B is finite if B is finitely generated as an A-module.

Русский

Кольцевое отображение f: A → B считается конечно порождаемым, если B конечно порождается как A-модуль.

LaTeX

$$RingHom.Finite f ⇔ Module.Finite A B$$

Lean4

/-- A ring morphism `A →+* B` is `RingHom.Finite` if `B` is finitely generated as `A`-module. -/
@[algebraize Module.Finite, stacks 0563]
def Finite (f : A →+* B) : Prop :=
  letI : Algebra A B := f.toAlgebra
  Module.Finite A B

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