Commit 2026-04-28 06:53 3086afaf

View on Github →

chore: redefine Nat.div2 Nat.bodd (#36970)

Estimated changes

Modified Mathlib/Computability/Primrec/Basic.lean

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Nat/Bits.lean

modified def Nat.bodd

modified theorem Nat.boddDiv2_eq

modified theorem Nat.bodd_add_div2

modified def Nat.div2

modified theorem Nat.div2_val

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Encodable/Basic.lean

Modified Mathlib/Logic/Equiv/Nat.lean