neg_zpow — Mathlib

English

Let α be a division monoid with distributive negation and let n ∈ Z be even. Then for every a ∈ α, (-a)^n = a^n.

Русский

Пусть α — делимый моноид с распределительным отрицанием, и n ∈ ℤ чётно. Тогда для каждого a ∈ α выполняется (-a)^n = a^n.

LaTeX

$$$\forall \alpha \ [\text{DivisionMonoid } \alpha]\ [\text{HasDistribNeg } \alpha],\ \forall a \in \alpha,\ \operatorname{Even}(n) \Rightarrow (-a)^n = a^n.$$$

Lean4

theorem neg_zpow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by rintro ⟨c, rfl⟩ a;
  simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]

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