selfZPow_of_neg — Mathlib

English

For nonpositive integer exponent, selfZPow equals a unit-like construction mk' with 1 and a power of x.

Русский

Для неположительного целочисленного показателя selfZPow соответствует mk' с 1 и степенью x.

LaTeX

$$$selfZPow(x,B)\{n\} = mk'(B,1,Submonoid.pow(x,|n|))$$$

Lean4

theorem selfZPow_of_neg {n : ℤ} (hn : n < 0) : selfZPow x B n = mk' _ (1 : R) (Submonoid.pow x n.natAbs) :=
  dif_neg hn.not_ge

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