Commit 2024-10-22 16:44 3fc88df1

View on Github →

chore: deprecate Nat.binaryRec_eq, rename Nat.binaryRec_eq' => Nat.binaryRec_eq (#18039)

Estimated changes

Modified Mathlib/Data/Nat/BinaryRec.lean

deleted theorem Nat.binaryRec_eq'

modified theorem Nat.binaryRec_eq

Modified Mathlib/Data/Nat/BitIndices.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Data/Nat/EvenOddRec.lean

Modified Mathlib/Data/Num/Lemmas.lean