abs_neg_one_pow

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#abs_neg_one_pow

English

For any natural n, |(-1)^n| = 1.

Русский

Для любого натурального n, |(-1)^n| = 1.

LaTeX

$$$|(-1)^{n}| = 1$$$

Lean4

theorem abs_neg_one_pow (n : ℕ) : |(-1 : α) ^ n| = 1 := by rw [← pow_abs, abs_neg, abs_one, one_pow]

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

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

Разделы

Аффилиация

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