inv_pow_sub₀ — Mathlib

English

If a ≠ 0 and n ≤ m are natural numbers, then (a^{-1})^{m-n} = (a^{m})^{-1} a^{n}. This expresses the law for negative/reciprocal powers in a GroupWithZero when a is nonzero.

Русский

Пусть a ≠ 0 и n ≤ m. Тогда (a^{-1})^{m-n} = (a^{m})^{-1} a^{n}. Это выражает закон для отрицательных степеней в группе с нулём при ненулевом a.

LaTeX

$$$\forall a \in G_0\setminus\{0\},\forall m,n \in \mathbb{N},\ n\le m\;:\; (a^{-1})^{m-n}=(a^{m})^{-1}a^{n}$$$

Lean4

theorem inv_pow_sub₀ (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n := by
  rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]

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