pow_sub — Mathlib

English

For a ∈ G and natural m ≥ n, a^{m-n} = a^{m} (a^{n})^{-1}.

Русский

Для любого a ∈ G и натуральных m ≥ n выполняется a^{m-n} = a^{m} (a^{n})^{-1}.

LaTeX

$$$\forall a \in G,\forall m,n \in \mathbb{N},\ n \le m \Rightarrow a^{(m-n)} = a^{m} (a^{n})^{-1}.$$

Lean4

@[to_additive sub_nsmul]
theorem pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
  eq_mul_inv_of_mul_eq <| by rw [← pow_add, Nat.sub_add_cancel h]

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