of_mem_closure — Mathlib

English

If a RingHom f is finite, then it is integral.

Русский

Если RingHom f конечен, то он интегральен.

LaTeX

$$$f^{\text{Finite}} \Rightarrow f^{\text{IsIntegral}}.$$$

Lean4

theorem of_mem_closure {x y z : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y)
    (hz : z ∈ Subring.closure ({ x, y } : Set S)) : f.IsIntegralElem z :=
  by
  letI : Algebra R S := f.toAlgebra
  have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)
  rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this
  exact
    IsIntegral.of_mem_of_fg (Algebra.adjoin R { x, y }) this z
      (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

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