cast_lt_intCast

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#Rat.cast_lt_intCast

English

For m ∈ ℚ and n ∈ ℤ, (m : K) < n ↔ m < n in ℚ.

Русский

Для m ∈ ℚ и n ∈ ℤ, (m : K) < n эквивалентно m < n в ℚ.

LaTeX

$$$ \forall {m : \mathbb{Q}} {n : \mathbb{Z}}, \ (m : K) < n.cast \leftrightarrow m < n.cast. $$$

Lean4

@[simp, norm_cast]
theorem cast_lt_intCast {m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ) := by rw [← cast_lt (K := K), cast_intCast]

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

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

Разделы

Аффилиация

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