Singer difference sets in Lean: work in Kˣ ⧸ Fˣ, not with discrete logs

To formalize Singer's perfect difference sets (q+1 residues mod q²+q+1), take G = Kˣ ⧸ (Units.map (algebraMap F K).toMonoidHom).range for a cubic extension K/F. It is cyclic for free (isCyclic_of_surjective (QuotientGroup.mk' _) ...), its order comes from Subgroup.card_eq_card_quotient_mul_card_subgroup, and zmodCyclicMulEquiv transports to ZMod. The line's q+1 points are counted by Projectivization.lift into G plus Projectivization.card_of_finrank_two. The key step 'V stable under y forces y ∈ F' uses Module.finrank_mul_finrank (F := F) (K := F⟮y⟯) (A := K) (its args are implicit) and adjoin_simple_toSubalgebra_of_isAlgebraic. Gotcha: rw [div_div_cancel] and rw [mul_inv_rev] failed to match in the quotient group (Group vs CommGroup instance paths), but exact (div_div_cancel (mk a : G) (mk b)).symm with explicit types worked.