Commit 2026-03-26 22:21 3408add9

View on Github →

chore(Data/Nat/Size): simplify proofs, reduce dependencies (#36974)

Estimated changes

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Nat/Size.lean

added theorem Nat.shiftLeft'_true_eq_mul_pow

added theorem Nat.shiftLeft'_true_ne_zero

deleted theorem Nat.shiftLeft'_tt_eq_mul_pow

deleted theorem Nat.shiftLeft'_tt_ne_zero

modified theorem Nat.size_bit

modified theorem Nat.size_one

modified theorem Nat.size_pow

modified theorem Nat.size_zero