negOnePow_abs

Mathlib.Algebra.Ring.NegOnePow

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

English

The arithmetic with absolute value commutes with negOnePow: |n|.negOnePow = n.negOnePow.

Русский

Абсолютное значение числа и операция negOnePow commute: |n|.negOnePow = n.negOnePow.

LaTeX

$$$|n|.negOnePow = n.negOnePow$$$

Lean4

@[simp]
theorem negOnePow_abs (n : ℤ) : |n|.negOnePow = n.negOnePow := by
  obtain h | h := abs_choice n <;> simp only [h, negOnePow_neg]

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

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

Разделы

Аффилиация

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