neg_zpow — Mathlib

English

If n is odd and a is in a division ring, then (-a)^n = -a^n.

Русский

Если n нечётное, то (-a)^n = -a^n в делительной кольце.

LaTeX

$$$\text{Odd}(n) \Rightarrow (-a)^n = -a^n$$$

Lean4

theorem neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n :=
  by
  have hn : n ≠ 0 := by rintro rfl; exact Int.not_even_iff_odd.2 h .zero
  obtain ⟨k, rfl⟩ := h
  simp_rw [zpow_add' (.inr (.inl hn)), zpow_one, zpow_mul, zpow_two, neg_mul_neg, neg_mul_eq_mul_neg]

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