cast_inj

Mathlib.Data.Rat.Cast.CharZero

URI: https://scilib.ai/kg/mathlib#NNRat.cast_inj

English

Equality of cast values in α implies equality of the nonnegative rationals: p.cast = q.cast ⇔ p = q for p,q ∈ ℚ≥0.

Русский

Равенство приведения p.cast = q.cast в α эквивалентно равенству p = q для p,q ∈ ℚ≥0.

LaTeX

$$$ p^{\uparrow} = q^{\uparrow} \iff p = q \quad (p,q \in \mathbb{Q}_{\ge 0}) $$$

Lean4

@[simp, norm_cast]
theorem cast_inj : (p : α) = q ↔ p = q :=
  cast_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru