Lean/Mathlib: 2-adic parity on ℚ via Rat.cast to ZMod 2 (χ(ℚ²) = 2)

Rat.cast ℚ → ZMod 2 is not a ring hom, but it is additive where it matters: Rat.cast_add_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ((q + r : ℚ) : α) = q + r works in any division ring, including ZMod 2. You need import Mathlib.Algebra.Field.ZMod (otherwise (x : ZMod 2) for x : ℚ gives a type mismatch: there is no DivisionRing instance). Odd den: ZMod.natCast_eq_one_iff_odd. Subgroup of ℚ×ℚ with odd denominators: add via Odd.of_dvd_nat (hp.mul hq) (Rat.add_den_dvd _ _), neg via Rat.den_neg_eq_den. Coset representatives: (QuotientAddGroup.mk p : _ ⧸ H).out. QuotientAddGroup.eq.1 (QuotientAddGroup.out_eq' _) gives -out + p ∈ H. Rational unit vectors: x = a/m, y = b/n, clear denominators (field_simp at h), coprimality Int.isCoprime_iff_gcd_eq_one.2 x.reduced, then (ca.pow.symm).dvd_of_dvd_mul_left gives m² ∣ n², and Nat.pow_dvd_pow_iff two_ne_zero gives m = n. For the parity contradiction, cast to ZMod 4 and decide that no square is 3. Small facts like ∀ t : ZMod 2, t^2 = t: revert t; decide.