abs_eq_natAbs

Mathlib.Algebra.Order.Group.Unbundled.Int

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

← MathLib Explorer

English

The absolute value of an integer equals its natAbs cast to ℤ.

Русский

Модуль целого числа равен преобразованию natAbs к целому число.

LaTeX

$$$ |n| = (\operatorname{natAbs}(n))_{\mathbb{Z}}. $$$

Lean4

theorem abs_eq_natAbs : ∀ a : ℤ, |a| = natAbs a
  | (n : ℕ) => abs_of_nonneg <| ofNat_zero_le _
  | -[_+1] => abs_of_nonpos <| le_of_lt <| negSucc_lt_zero _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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