mathlib3

3c227fc0 - feat(data/nat/parity): add lemmas nat.bit{0|1}_mod_bit0 (#16396)

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](https://leanprover-community.github.io/mathlib_docs/data/nat/parity.html#nat.bit0_div_bit0) and [nat.bit1_div_bit0](https://leanprover-community.github.io/mathlib_docs/data/nat/parity.html#nat.bit1_div_bit0), namely ```lean @[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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/bit0.2Fbit1.20and.20mod/near/297228893)