to_isIntegral — Mathlib

English

For any rings R,S with a ring hom f: R → S that is finite as an R-module, f is integral.

Русский

Если кольца R,S и гомоморфизм f: R → S является конечным как модуль над R, то f интегрально.

LaTeX

$$$f: R \to S \text{ is finite} \Rightarrow f \text{ is integral}.$$$

Lean4

@[stacks 00GK]
theorem to_isIntegral (h : f.Finite) : f.IsIntegral :=
  letI := f.toAlgebra
  fun _ ↦ IsIntegral.of_mem_of_fg ⊤ h.1 _ trivial

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