zpow_sub_one — Mathlib

English

Let a be an element of a group G. For every integer n, a^(n-1) = a^n a^{-1}.

Русский

Пусть a принадлежит группе G. Для любого целого n выполняется a^(n-1) = a^n a^{-1}.

LaTeX

$$$\forall a \in G,\ \forall n \in \mathbb{Z},\ a^{n-1} = a^{n} a^{-1}$$$

Lean4

@[to_additive sub_one_zsmul]
theorem zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := (mul_inv_cancel_right _ _).symm
    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one, Int.sub_add_cancel]

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