Commit 2025-07-04 01:43 f510df87

View on Github →

chore(Data/*): remove various erw (#26711) This PR addresses tech debt by eliminating some erw in the Data directory

Estimated changes

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Nat/Bitwise.lean

added theorem Nat.bit_false_apply

added theorem Nat.bit_true_apply

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Num/ZNum.lean

Modified Mathlib/Data/Vector/Basic.lean