pow — Mathlib

English

Power on WithZero α is defined by: (0 : WithZero α) has the usual 0-power behavior, and (some a) behaves by the underlying α-power: (some a)^n = a^n; 0^0 = 1; 0^{n+1} = 0; 0^{Int.negSucc _} = 0.

Русский

Степень в WithZero α определяется так: 0^0 = 1, 0^{n+1} = 0, а (ноль не нуль) = (a)^n для некоторого a ∈ α; 0^{n} для n>0 равно 0; целочисленные степени для 0 и для элементов α задаются аналогично.

LaTeX

$$$(0 : WithZero \\alpha)^{0} = 1,\quad (0 : WithZero \\alpha)^{n+1} = 0,\quad (a : \\alpha)^{n} = a^{n}. $$$

Lean4

instance pow : Pow (WithZero α) ℕ where
  pow
    | none, 0 => 1
    | none, _ + 1 => 0
    | some x, n => ↑(x ^ n)

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