divInt_eq_zero

Mathlib.Data.Rat.Defs

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

← MathLib Explorer

English

Let a,b ∈ ℤ with b ≠ 0. Then a /. b = 0 iff a = 0.

Русский

Пусть a,b ∈ ℤ и b ≠ 0. Тогда a /. b = 0 ⇔ a = 0.

LaTeX

$$$ \forall \{a,b : \mathbb{Z}\}, b \neq 0 \rightarrow (a /. b) = 0 \leftrightarrow a = 0 $$$

Lean4

@[simp]
theorem divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0 := by
  rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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