Theorems · Theorem · logic and foundations

ONote.opowAux.eq_def

∀ (e a0 a : ONote) (x x_1 : ℕ),
  e.opowAux a0 a x x_1 =
    match x, x_1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

0 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext