roots_mem_integralClosure — Mathlib

English

If f ∈ R[X] is monic and a ∈ S is a root of f in S, then a lies in the integral closure of R in S.

Русский

Если f ∈ R[X] моноическая и a ∈ S является корнем f в S, то a принадлежит интегральному замыканию R в S.

LaTeX

$${f : R[X]} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) : a ∈ integralClosure R S$$

Lean4

theorem roots_mem_integralClosure {f : R[X]} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) : a ∈ integralClosure R S :=
  ⟨f, hf, (eval₂_eq_eval_map _).trans <| (mem_roots <| (hf.map _).ne_zero).1 ha⟩

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