∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α] (ψ : AddChar α ℂ),
  (fun ψ => AddChar.toMonoidHomEquiv.symm (Circle.coeHom.comp ψ.toMonoidHom))
      ((fun ψ => { toFun := fun a => ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }) ψ) =
    ψ