natCast_natAbs

Mathlib.Algebra.Order.Group.Unbundled.Int

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

English

Taking natAbs of an absolute value preserves natAbs.

Русский

Преобразование natAbs от положительного числа сохраняет natAbs.

LaTeX

$$$ \operatorname{natAbs}(|a|) = \operatorname{natAbs}(a). $$$

Lean4

@[norm_cast]
theorem natCast_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| :=
  n.abs_eq_natAbs.symm

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

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

Разделы

Аффилиация

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