Commit 2022-09-06 14:33 3c227fc0
View on Github →feat(data/nat/parity): add lemmas nat.bit{0|1}_mod_bit0 (#16396) This PR adds a pair of lemmas that complement nat.bit0_div_bit0 and nat.bit1_div_bit0, namely
@[simp] lemma bit0_mod_bit0 : bit0 n % bit0 m = bit0 (n % m) := ...
@[simp] lemma bit1_mod_bit0 : bit1 n % bit0 m = bit1 (n % m) := ...
They will be helpful in an upcoming PR that introduces a norm_num extension for computing Jacobi symbols.
Zulip thread