instPowInt — Mathlib

English

There is a power operation on WithZero α by integers: for a ∈ α and n ∈ ℤ, (↑a)^n is defined as in α for nonzero a, and 0 for zero-exponent cases as above.

Русский

Существует операция возведения в степень над WithZero α на целых: для a ∈ α и n ∈ ℤ определяется (↑a)^n так же, как в α, для нулевого элемента — как в соответствующей схеме.

LaTeX

$$$\\text{Pow}_{WithZero}(a, n) \\;\\text{определено так:}$ \n\\text{(0) }^{0} = 1,\\ (0)^{|\\mathrm{Int}(|n|)|} = 0,\\ (a)^{n} = \\uparrow(a^{n})$ для $a \\in α$, $n ∈ \\mathbb{Z}$.$$

Lean4

instance : Pow (WithZero α) ℤ where
  pow
    | none, Int.ofNat 0 => 1
    | none, Int.ofNat (Nat.succ _) => 0
    | none, Int.negSucc _ => 0
    | some x, n => ↑(x ^ n)

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