finiteType — Mathlib

English

If f : A →ₐ[R] B is a finite (as a ring homomorphism) then f is of finite type as an algebra homomorphism.

Русский

Если гомоморфизм Алгебра A → B конечен как кольцевой гомоморфизм, он имеет конечный тип как гомоморфизм алгебр.

LaTeX

$$finiteType {f : A →ₐ[R] B} (hf : f.Finite) : FiniteType f$$

Lean4

theorem finiteType {f : A →ₐ[R] B} (hf : f.Finite) : FiniteType f :=
  RingHom.Finite.finiteType hf

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