cast_negSucc

Mathlib.Data.Int.Cast.Basic

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

English

For any natural n, the cast of −(n+1) equals −(n+1) in any AddGroupWithOne R.

Русский

Для любого натурального n отображение −(n+1) в R равно −(n+1).

LaTeX

$$$\text{(-}(n+1)\text{ : ℤ) } \text{ cast to } R = -(n+1)\,$$

Lean4

@[simp, norm_cast squash]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
  AddGroupWithOne.intCast_negSucc n

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

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

Разделы

Аффилиация

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