Rational combinations of 1 and an irrational element #
Let K be a division ring of characteristic zero and let β ∈ K be irrational, that is, not the
image of a rational number. Then the rational combinations a + b β are pairwise distinct
(TauCeti.ratCast_add_ratCast_mul_injective): the map (a, b) ↦ a + b β from ℚ × ℚ to K is
injective. For example, the integer grid points u + v β used in transcendence proofs are
distinct.
theorem
TauCeti.ratCast_add_ratCast_mul_injective
{K : Type u_1}
[DivisionRing K]
[CharZero K]
{β : K}
(hβ : ∀ (q : ℚ), ↑q ≠ β)
:
Rational combinations of 1 and an irrational element are distinct: if β in a division
ring of characteristic zero is not the image of a rational number, then (a, b) ↦ a + b β is
injective on ℚ × ℚ.