Rational algebraic integers

ℤ is integrally closed in ℚ, so an algebraic integer that happens to be rational is an integer. This file records the numerical reading of that fact: an identity n · z = m between an algebraic integer z and two natural numbers is a divisibility n ∣ m. It holds over an arbitrary field of characteristic zero, z = m / n being the image of a rational number there and integrality descending along algebraMap ℚ k.

Main results

• TauCeti.dvd_of_isIntegral_of_natCast_mul_eq: if (n : k) * z = m with z integral over ℤ in a field of characteristic zero and n ≠ 0, then n ∣ m.

theorem TauCeti.dvd_of_isIntegral_of_natCast_mul_eq {k : Type u_1} [Field k] [CharZero k] {m n : ℕ} {z : k} (hz : IsIntegral ℤ z) (h : ↑n * z = ↑m) (hn : n ≠ 0) : n ∣ m

A rational algebraic integer is an integer, read as a divisibility: if n · z = m for natural numbers m and n with n ≠ 0, and z is integral over ℤ in a field of characteristic zero, then n divides m.