divInt_one

Mathlib.Data.Rat.Defs

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

English

For any n ∈ ℤ, n /. 1 = n.cast.

Русский

Для любого n ∈ ℤ, n /. 1 = n.cast.

LaTeX

$$$ \forall n \in \mathbb{Z}, n /. 1 = n.cast $$$

Lean4

@[simp]
theorem divInt_one (n : ℤ) : n /. 1 = n := by simp [divInt, mkRat, normalize]

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

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

Разделы

Аффилиация

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