Finite — Mathlib

English

An algebra homomorphism f: A →ₐ[R] B is finite if and only if the underlying ring homomorphism f.toRingHom is finite.

Русский

Альгебра-гомоморфизм f: A →ₐ[R] B считается конечным тогда и только тогда, когда соответствующее кольцевое отображение f.toRingHom конечное.

LaTeX

$$AlgHom.Finite f ↔ f.toRingHom.Finite$$

Lean4

/-- An algebra morphism `A →ₐ[R] B` is finite if it is finite as ring morphism.
In other words, if `B` is finitely generated as `A`-module. -/
def Finite (f : A →ₐ[R] B) : Prop :=
  f.toRingHom.Finite

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