inv_pow_sub_of_lt — Mathlib

English

For a ∈ G_0 and m,n ∈ ℕ with n < m, we have (a^{-1})^{m-n} = (a^{m})^{-1} a^{n}. No extra nonzero assumption on a is needed here since the statement is written for all a in the group with zero.

Русский

Пусть a ∈ G_0 и n,m ∈ ℕ с n < m. Тогда (a^{-1})^{m-n} = (a^{m})^{-1} a^{n}.

LaTeX

$$$\forall a \in G_0,\forall m,n\in\mathbb{N},\ n

Lean4

theorem inv_pow_sub_of_lt (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n := by
  rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]

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