mk_num_ne_zero_of_ne_zero

Mathlib.Data.Rat.Defs

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

English

If q ≠ 0 and q = n/d with integers n,d, then n ≠ 0.

Русский

Если q ≠ 0 и q = n/d при целых n,d, то n ≠ 0.

LaTeX

$$$q \neq 0 \wedge q = \dfrac{n}{d} \Rightarrow n \neq 0$$$

Lean4

theorem mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0 := fun this =>
  hq <| by simpa [this] using hqnd

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

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

Разделы

Аффилиация

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