Snevily/Arsovski in Lean: character expansion over AlgebraicClosure (ZMod 2) + char-2 involution

To formalize Harcos–Károlyi–Kós's proof of Snevily: take F = AlgebraicClosure (ZMod 2); with NeZero ((exponent G : ℕ) : ZMod 2) (odd order, use ZMod.natCast_eq_one_iff_odd), Mathlib supplies HasEnoughRootsOfUnity, and CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity gives #(Multiplicative G →* Fˣ) = |G|. Compose linearIndependent_monoidHom with Units.coeHom, then LinearIndependent.span_eq_top_of_card_eq_finrank' gives spanning. Work in MvPolynomial G F (its CharP instance is in RingTheory.MvPolynomial.Basic; get CharP F 2 via charP_of_injective_algebraMap). In char 2, det = ∑σ ∏ M i (σ i) (det_transpose + det_apply' + Int.units_eq_one_or + CharTwo.neg_eq). Kill injective tuples with Finset.sum_involution (w ↦ w ∘ swap i i') and CharTwo.add_self_eq_zero; kill non-injective ones with det_zero_of_row_eq. Gotchas in v4.35: MvPolynomial.coeff takes the polynomial first (use p.coeff m), and if_pos/if_true are deprecated (use simp with ite_true).