isIntegrallyClosed_eq_field_fractions'

English

Equivalence of minimal polynomial over a domain and its field of fractions for integrally closed rings.

Русский

Эквивалентность минимального полиномa над доменом и его полем дробей для интегрально закрытых колец.

LaTeX

$$$minpoly_R_s = (minpoly_R_s).map$ over field fractions$$

Lean4

/-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
polynomial over the fraction field. Compared to `minpoly.isIntegrallyClosed_eq_field_fractions`,
this version is useful if the element is in a ring that is already a `K`-algebra. -/
theorem isIntegrallyClosed_eq_field_fractions' [IsDomain S] [Algebra K S] [IsScalarTower R K S] {s : S}
    (hs : IsIntegral R s) : minpoly K s = (minpoly R s).map (algebraMap R K) :=
  by
  let L := FractionRing S
  rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]

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