gnpowRec — Mathlib

English

The zero power yields the identity: gnpowRec 0 a = 1.

Русский

Нулевая степень даёт единицу: gnpowRec 0 a = 1.

LaTeX

$$$\mathrm{gnpowRec}(0, a) = 1$$$

Lean4

/-- A default implementation of power on a graded monoid, like `npowRec`.
`GMonoid.gnpow` should be used instead. -/
def gnpowRec : ∀ (n : ℕ) {i}, A i → A (n • i)
  | 0, i, _ => cast (congr_arg A (zero_nsmul i).symm) GOne.one
  | n + 1, i, a => cast (congr_arg A (succ_nsmul i n).symm) (GMul.mul (gnpowRec _ a) a)

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