Anomaly Coefficient of reduce

lemma anomalyCoefficient_of_reduce (F : FiveQuanta 𝓩) [DecidableEq 𝓩] :    F.reduce.anomalyCoefficient = F.anomalyCoefficient := by  have reduce_sum_N_mul_eq : ∀ h : 𝓩 → 𝓩, (F.reduce.map fun x => (x.2.N : 𝓩) * h x.1).sum =      (F.map fun x => (x.2.N : 𝓩) * h x.1).sum := by    intro h    let f : 𝓩 → Fluxes →+ 𝓩 := fun q5 =>      { toFun := fun x => x.N • h q5        map_zero' := by simp        map_add' := by          intros x y          simp [add_mul] }    simpa [f] using reduce_sum_eq_sum_toCharges F f  simp [anomalyCoefficient]  exact ⟨reduce_sum_N_mul_eq fun q => q, reduce_sum_N_mul_eq fun q => q * q⟩