neg_pow — Mathlib

English

Let α be a monoid with distributive neg. If n is odd, then (-a)^n = -a^n for all a.

Русский

Пусть α — моноид с распределительным отрицанием. Если n нечетно, то (-a)^n = -a^n для всех a.

LaTeX

$$$\operatorname{Odd}(n) \rightarrow \forall a,\ (-a)^n = -a^n$$$

Lean4

theorem neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n := by rintro ⟨c, rfl⟩ a;
  simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

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