Theorems · Theorem · commutative algebra

IsAlgebraic.exists_smul_eq

∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] {K : Type u_4} [inst_2 : CommRing K]
  [inst_3 : Algebra S K] [inst_4 : Algebra R K] [IsIntegralClosure S R K] {x : K},
  IsAlgebraic R x → ∃ r s, r ≠ 0 ∧ r • x = (algebraMap S K) s

If x : K is algebraic over some ring R, then a nonzero R-multiple of it is contained in the integral closure of R in K.

Defined in

Mathlib.RingTheory.Algebraic.Integral

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebraIsIntegralClosure