to_finite — Mathlib

English

If f is integral and of finite type, then f is finite as a ring extension.

Русский

Если отображение f интегрально и имеет конечный тип, тогда оно конечное как расширение колец.

LaTeX

$$$f.IsIntegral \\Rightarrow f.FiniteType \\Rightarrow f.Finite$$$

Lean4

theorem to_finite (h : f.IsIntegral) (h' : f.FiniteType) : f.Finite :=
  let _ := f.toAlgebra
  let _ : Algebra.IsIntegral R S := ⟨h⟩
  Algebra.IsIntegral.finite (h' := h')

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