English
There is a default way to interpret integers in any AddGroupWithOne: nonnegative integers map to themselves and negative numbers map to the negation of their successor.
Русский
Существует стандартное отображение целых чисел в любую AddGroupWithOne: неотрицательные числа отображаются как сами числа, отрицательные — как противоположности их единичному преемнику.
LaTeX
$$$\text{Int.castDef} : \mathbb{Z} \to R \,; \; (n \ge 0) \mapsto n,\; (-\! ) \mapsto -\text{succ}$$$
Lean4
/-- Default value for `IntCast.intCast` in an `AddGroupWithOne`. -/
protected def castDef {R : Type u} [NatCast R] [Neg R] : ℤ → R
| (n : ℕ) => n
| Int.negSucc n => -(n + 1 : ℕ)
