BohrSet.eq_zero_of_ewidth_eq_zero

lemma eq_zero_of_ewidth_eq_zero {B : BohrSet G} [Finite G] (h : B.ewidth = 0) :    B.chordSet = {0} := by  rw [Set.eq_singleton_iff_unique_mem]  simp only [mem_chordSet_iff_nnnorm_width, map_zero_eq_one, sub_self, nnnorm_zero, zero_le,    implies_true, true_and]  intro x hx  by_contra!  rw [←AddChar.exists_apply_ne_zero] at this  obtain ⟨ψ, hψ⟩ := this  apply hψ  have hψ' : ψ ∈ B.frequencies := by simp [B.mem_frequencies, h]  specialize hx hψ'  rwa [B.width_def, h, Pi.zero_apply, ENNReal.toNNReal_zero, nonpos_iff_eq_zero, nnnorm_eq_zero,    sub_eq_zero, eq_comm] at hx