pow_sub₀ — Mathlib

English

Let a ≠ 0 and n ≤ m. Then a^{m-n} = a^{m} (a^{n})^{-1}.

Русский

Пусть a ≠ 0 и n ≤ m. Тогда a^{m-n} = a^{m} (a^{n})^{-1}.

LaTeX

$$$ (a \\neq 0) \\land (n \\le m) \\Rightarrow a^{(m-n)} = a^{m} (a^{n})^{-1} $$$

Lean4

theorem pow_sub₀ (a : G₀) (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
  by
  have h1 : m - n + n = m := Nat.sub_add_cancel h
  have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
  simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2

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