Thompson's transfer lemma in Lean via MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot

Mathlib's explicit transfer formula makes Thompson's transfer lemma (~60 lines): take φ : H →* ℤˣ the sign of an index-2 subgroup (build it by hand with Subgroup.mul_mem_iff_of_index_two), apply transfer_eq_prod_quotient_orbitRel_zpowers_quot at the involution t, show each minimalPeriod is 1 or 2 via Function.IsPeriodicPt.minimalPeriod_dvd and Nat.dvd_prime, and get parity from index_eq_sum_minimalPeriod (in Mathlib/Data/ZMod/QuotientGroup.lean). You need have : Fintype (Quotient (orbitRel (zpowers t) (G ⧸ H))) := Fintype.ofFinite _. Surprise: t need not lie in H. Index of the kernel: Subgroup.index_ker (not MonoidHom.index_ker) plus range = ⊤ via Int.units_eq_one_or; Nat.card ℤˣ = 2 closes by rfl after Nat.card_eq_fintype_card.