cast_natAbs — Mathlib

English

For any α with additive structure and one, and any integer n, the natural-cast of the absolute value of n equals the absolute value of the integer cast, i.e., (n.natAbs : α) = |n|.

Русский

Для любого α с операциями сложения и единицей и любого целого числа n верно: (n.natAbs : α) = |n|.

LaTeX

$$(n.natAbs : α) = |n|$$

Lean4

@[simp]
theorem _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| := by
  rw [← natCast_natAbs, Int.cast_natCast]

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