cast_negOfNat

Mathlib.Data.Int.Cast.Basic

URI: https://scilib.ai/kg/mathlib#Int.cast_negOfNat

English

For any m,n, the cast of m − n equals m − n in any AddGroupWithOne R.

Русский

Для любых m,n отображение m − n в R равно m − n.

LaTeX

$$$(m - n : \mathbb{Z}) : R = m - n$$$

Lean4

@[simp]
theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n := by simp [Int.cast_neg, negOfNat_eq]

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

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

Разделы

Аффилиация

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