English
The embedding ℚ → α is injective for any DivisionRing α of characteristic zero.
Русский
Вставка ℚ в α инъективна для любого делимого кольца α характеристика ноль.
LaTeX
$$$ \uparrow p = \uparrow q \Rightarrow p = q \quad (p,q \in \mathbb{Q}) $$$
Lean4
@[stacks 09FR "Characteristic zero case."]
theorem cast_injective : Injective ((↑) : ℚ → α)
| ⟨n₁, d₁, d₁0, c₁⟩, ⟨n₂, d₂, d₂0, c₂⟩, h =>
by
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
rw [mk'_eq_divInt, mk'_eq_divInt] at h ⊢
rw [cast_divInt_of_ne_zero, cast_divInt_of_ne_zero] at h <;> simp [d₁0, d₂0] at h ⊢
rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq, ← mul_assoc, ←
division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁, ← Int.cast_mul, ←
Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0] at h
