pow_sub_of_lt — Mathlib

English

Let G be a GroupWithZero and m,n be natural numbers with n < m. Then for any a ∈ G, a^{m-n} equals a^{m} multiplied by the inverse of a^{n}. In particular, the usual exponent law a^{m-n} = a^{m} (a^{n})^{-1} holds (with the edge case a = 0 handled separately).

Русский

Пусть G — группа с нулём и целые числа m,n натуральные, причем n < m. Тогда для любого a ∈ G выполняется a^{m-n} = a^{m} (a^{n})^{-1}. В случае a = 0 рассматривается отдельный случай для корректности формулы.

LaTeX

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

Lean4

theorem pow_sub_of_lt (a : G₀) (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
  by
  obtain rfl | ha := eq_or_ne a 0
  · rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by cutsat), zero_mul]
  · exact pow_sub₀ _ ha <| Nat.le_of_lt h

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