divInt_neg

Mathlib.Data.Rat.Defs

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

English

n /. -d = -n /. d for all n,d ∈ ℤ.

Русский

n /. -d = -n /. d для всех n,d ∈ ℤ.

LaTeX

$$$ \forall (n d : \mathbb{Z}), n /. -d = -n /. d $$$

Lean4

@[simp]
theorem divInt_neg (n d : ℤ) : n /. -d = -n /. d :=
  divInt_neg' ..

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

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

Разделы

Аффилиация

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