zpow_natCast_sub_natCast₀ — Mathlib

English

If a ≠ 0 and m,n ∈ ℕ, then a^{(m-n)} = a^{m} / a^{n} when interpreted in ℤ via the natural-cast sub, i.e., zpow_sub₀ reduces to this case.

Русский

Если a ≠ 0 и m,n ∈ ℕ, то a^{(m-n)} = a^{m} / a^{n} в случае преобразования через целочисленное zpow с преобразованием из натурального.

LaTeX

$$$\forall a\neq 0,\forall m,n\in\mathbb{N}: a^{(m-n)} = a^{m} / a^{n}$$$

Lean4

theorem zpow_natCast_sub_natCast₀ (ha : a ≠ 0) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n := by
  simpa using zpow_sub₀ ha m n

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