cast_injective — Mathlib

English

Injectivity of the embedding ((↑) : ℚ≥0 → α) for DivisionSemiring α with CharZero.

Русский

Инъективность отображения ((↑) : ℚ≥0 → α) для DivisionSemiring α с CharZero.

LaTeX

$$$ \forall p,q: \mathbb{Q}_{\ge 0},\; p \uparrow = q \uparrow \Rightarrow p = q. $$$

Lean4

theorem cast_injective : Injective ((↑) : ℚ≥0 → α) :=
  by
  rintro p q hpq
  rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
  on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
  · norm_cast at hpq ⊢
  any_goals norm_cast
  any_goals apply den_ne_zero
  exact Nat.cast_commute ..

Похожие утверждения