Theorems · Definition · commutative algebra

Algebra.denominator

(R : Type u_1) →
  {S : Type u_2} → [inst : CommRing R] → [IsPrincipalIdealRing R] → [inst_2 : CommRing S] → [Algebra R S] → S → R

The denominator of an element x of an R-algebra: a generator of the ideal of scalars r : R such that r • x is integral over R. It is nonzero as soon as x is algebraic over R; see IsAlgebraic.denominator_ne_zero.

Defined in

Mathlib.RingTheory.Algebraic.Denominator

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingCommRingAlgebra