npowRec_eq_npowBinRec — Mathlib

English

Equivalence of two exponentiation frameworks npowRecAuto and npowBinRecAuto.

Русский

Эквивалентность двух фреймворков возведения в степень: npowRecAuto = npowBinRecAuto.

LaTeX

$$$\\text{npowRec_eq_npowBinRec}$$$

Lean4

@[to_additive (attr := csimp)]
theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto :=
  by
  funext M _ _ k m
  rw [npowBinRecAuto, npowRecAuto, npowBinRec]
  match k with
  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
  | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]

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