zpow_sub₀ — Mathlib

English

For a ≠ 0 and m,n ∈ ℤ, we have a^{m-n} = a^{m} / a^{n}. This is the integer-power subtraction rule for a nonzero base.

Русский

Пусть a ≠ 0 и m,n ∈ ℤ. Тогда a^{m-n} = a^{m} / a^{n}. Это правило различий по целочисленным степеням с ненулевой основой.

LaTeX

$$$\forall a\neq 0,\forall m,n\in\mathbb{Z}: a^{m-n}=\dfrac{a^{m}}{a^{n}}$$$

Lean4

theorem zpow_sub₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m - n) = a ^ m / a ^ n := by
  rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]

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