selfZPow_of_nonpos — Mathlib

English

For nonnegative exponent, selfZPow coincides with the usual power x^n mapped into the localization.

Русский

Для неотрицательного показателя selfZPow совпадает с обычной степенью x^n в локализации.

LaTeX

$$$selfZPow(x,B,n) = (algebraMap(R,B)\ x)^n$ for n ≥ 0$$

Lean4

theorem selfZPow_of_nonpos {n : ℤ} (hn : n ≤ 0) : selfZPow x B n = mk' _ (1 : R) (Submonoid.pow x n.natAbs) :=
  by
  by_cases hn0 : n = 0
  · simp [hn0, selfZPow_zero, Submonoid.pow_apply]
  · simp [selfZPow_of_neg _ _ (lt_of_le_of_ne hn hn0)]

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