cast_negOnePow — Mathlib

English

For any division ring K and any integer n, the element n.negOnePow equals (-1)^n in K.

Русский

Для любого кольца делений K и целого числа n выполняется n.negOnePow = (-1)^n в K.

LaTeX

$$$\forall n\in\mathbb{Z},\ n.negOnePow = (-1)^{n}$$$

Lean4

theorem cast_negOnePow (K : Type*) (n : ℤ) [DivisionRing K] : n.negOnePow = (-1 : K) ^ n :=
  by
  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
  · simp [zpow_mul, zpow_ofNat]
  · rw [zpow_add_one₀ (by simp), zpow_mul, zpow_ofNat]
    simp

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