Conversation
PR summary bf9280f5f2
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Init.Data.Nat.Basic | 39 | 7 | -32 (-82.05%) |
| Mathlib.Init.Data.Nat.Lemmas | 43 | 12 | -31 (-72.09%) |
| Mathlib.Data.Num.Prime | 544 | 543 | -1 (-0.18%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Init.Data.Nat.Basic |
-32 |
Mathlib.Init.Data.Nat.Lemmas |
-31 |
Mathlib.Data.Num.Prime |
-1 |
Declarations diff
+-+- not_even_bit1
+-+- pointReflection_fixed_iff_of_injective_bit0
+-+--+ bit1_of_bit1
+--+-+- cast_bit0
+--+-+- cast_bit1
- bit0_apply_eq_zero
- bit0_comp
- bit0_div_bit0
- bit0_div_two
- bit0_eq_bit0
- bit0_eq_two_mul
- bit0_mod_bit0
- bit0_zero
- bit1
- bit1_apply_eq_one
- bit1_comp
- bit1_div_bit0
- bit1_div_two
- bit1_eq_bit1
- bit1_mod_bit0
- bit1_zero
- coeff_cos_bit0
- coeff_cos_bit1
- coeff_sin_bit0
- coeff_sin_bit1
- even_bit0
- fib_bit0
- fib_bit0_succ
- fib_bit1
- fib_bit1_succ
- odd_bit1
- one_eq_bit1
- pow_bit0_nonneg
- pow_bit0_pos
- pow_bit0_pos_iff
- pow_bit1_neg_iff
- pow_bit1_nonneg_iff
- pow_bit1_nonpos_iff
- pow_bit1_pos_iff
- strictMono_pow_bit1
- two_dvd_bit0
- two_dvd_bit1
- zero_eq_bit0
- zpow_bit0_abs
-+- bit0_ne_bit1
-+- bit0_ne_zero
-+- bit1_ne_bit0
-+- bit1_ne_zero
-+- zero_ne_bit0
-+-+-+ bit0_of_bit0
-- bit0
-- bit0_val
-- bit1_eq_one
-- bit1_val
-- bodd_bit0
-- bodd_bit1
--++ bit_to_nat
--+- bit0_eq_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>| @@ -467,20 +467,20 @@ theorem pointReflection_involutive (x : P) : Involutive (pointReflection x : P | |||
| set_option linter.deprecated false | |||
There was a problem hiding this comment.
I'm guessing all of those can go now
There was a problem hiding this comment.
I would like to keep this diff as small as possible. And I also think that many of these lemmas can be removed or renamed in a second pass.
remove deprecated lemmas and simp tags
|
Closing, as #14745 is the version that shall be merged. |
This PR replaces
bit0 xresp.bit1 xwith:2 * xresp.2 * x + 1if possible, or2 • xresp.2 • x + 1if possible, orx + xresp.x + x + 1as fallback.The versions
Num.bit0andNum.bit1(as well as thePosNumandZNumversions) are left alone.All lemmas that mention
bit0/bit1have been adapted. A follow-up PR can remove these lemmas.Deletions: