Denominators of integral elements

The denominator Algebra.natDenominator x of an element x of a commutative ring is the absolute value of a generator of the ideal of integers n with n • x integral over ℤ (Algebra.natDenominator_dvd_iff); it is 0 when x is transcendental over ℤ. The denominator of x is 1 exactly when x is itself integral over ℤ (Algebra.natDenominator_eq_one_iff), that is, when every integer multiple of x is integral over ℤ. In a ℚ-algebra, an element algebraic over ℚ is algebraic over ℤ, so it has a nonzero denominator (Algebra.natDenominator_ne_zero_of_isAlgebraic_rat), and the denominator of a transcendental element is 0: over any commutative ring the denominator is nonzero exactly for elements algebraic over ℤ (Algebra.natDenominator_ne_zero_iff_isAlgebraic), and in a ℚ-algebra exactly for elements algebraic over ℚ (Algebra.natDenominator_ne_zero_iff_isAlgebraic_rat).

Main results

• Algebra.natDenominator_eq_one_iff: natDenominator x = 1 iff x is integral over ℤ.
• Algebra.natDenominator_ne_zero_of_isAlgebraic_rat: the denominator of an element of a ℚ-algebra that is algebraic over ℚ is nonzero.
• Algebra.natDenominator_ne_zero_iff_isAlgebraic: the denominator of x is nonzero exactly when x is algebraic over ℤ.
• Algebra.natDenominator_ne_zero_iff_isAlgebraic_rat: in a ℚ-algebra, the denominator of x is nonzero exactly when x is algebraic over ℚ.

@[simp]

theorem Algebra.natDenominator_eq_one_iff {S : Type u_1} [CommRing S] {x : S} : natDenominator x = 1 ↔ IsIntegral ℤ x

The denominator of x is one exactly when x is integral over ℤ: then every integer multiple of x is integral over ℤ.

theorem Algebra.natDenominator_ne_zero_of_isAlgebraic_rat {S : Type u_1} [CommRing S] [Algebra ℚ S] {x : S} (hx : IsAlgebraic ℚ x) : natDenominator x ≠ 0

The denominator of x is nonzero when x is algebraic over ℚ: in a ℚ-algebra, being algebraic over ℚ and being algebraic over ℤ are equivalent.

theorem Algebra.natDenominator_ne_zero_iff_isAlgebraic {S : Type u_1} [CommRing S] {x : S} : natDenominator x ≠ 0 ↔ IsAlgebraic ℤ x

The denominator of x is nonzero exactly when x is algebraic over ℤ; a transcendental element has denominator 0.

theorem Algebra.natDenominator_ne_zero_iff_isAlgebraic_rat {S : Type u_1} [CommRing S] [Algebra ℚ S] {x : S} : natDenominator x ≠ 0 ↔ IsAlgebraic ℚ x

In a ℚ-algebra, the denominator of x is nonzero exactly when x is algebraic over ℚ.