Commit 2026-08-12 18:02 5af8cdaf

feat(Algebra/Ring/Int/Parity): add Int.sq_emod_four and relocate square-mod-four lemma (#42296) Add Int.sq_emod_four : b ^ 2 % 4 = b % 2, and move the existing Int.sq_mod_four_eq_one_of_odd and (Nat/Int).eight_dvd_sq_sub_one_of_odd from NumberTheory.Multiplicity to the basic Parity files, their natural home. Also rename Int.sq_mod_four_eq_one_of_odd to Int.sq_emod_four_eq_one_of_odd and golf some proofs