Commit 2026-01-29 11:07 8d5a50dc

View on Github →

feat(Data/Nat): kernel reducible binaryRec (#30144)

  • Redefine Nat.binaryRec to allow kernel reduction.
  • Move some lemmas from Data/Nat/Bitwise to Data/Nat/BinaryRec.
  • Use nsmulBinRec for nsmul/zsmul on elliptic curves.

Estimated changes

added theorem npowBinRec_succ
added theorem npowBinRec_zero
added theorem Nat.bit_false
added theorem Nat.bit_false_apply
added theorem Nat.bit_ne_zero_iff
added theorem Nat.bit_true
added theorem Nat.bit_true_apply
modified theorem Nat.one_bits
deleted theorem Nat.bit_false
deleted theorem Nat.bit_false_apply
deleted theorem Nat.bit_ne_zero_iff
deleted theorem Nat.bit_true
deleted theorem Nat.bit_true_apply
modified def Nat.digitsAux
modified theorem Nat.digitsAux_zero