Repeated derivative of a complex function

Stream: new members

[Mark Gerads]

I need help with the nth derivative of a complex function, f:ℂ->ℂ, where n is in ℕ.
exponential_sum.lean
I got this error:
exponential_sum.lean:45:2
failed to synthesize type class instance for
k : ℕ+,
z : ℂ
⊢ normed_group ℂ
exponential_sum.lean:45:2
failed to synthesize type class instance for
k : ℕ+,
z : ℂ
⊢ nondiscrete_normed_field ℂ

I suspect this means that no one has implemented the iterated derivative on a complex function before. Please help. How do I show L∃∀N how to synthesize type class instances for [normed_group ℂ] and [nondiscrete_normed_field ℂ]? Would someone more skilled be interested in implementing this?

EDIT: I am currently looking at https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#type-classes-and-instances for the first time. Perhaps the syntax for instances is easier than I suspected.

[Mark Gerads]

This works, but these need to be formalized and added to mathlib:
instance normed_group_complex : normed_group ℂ :=
begin
sorry
end

instance nondiscrete_normed_field_complex : nondiscrete_normed_field ℂ :=
begin
sorry
end

instance normed_space_complex_complex : normed_space ℂ ℂ :=
begin
sorry
end

[Thomas Browning]

in analysis/complex/basic, I found this:

instance : normed_group ℂ :=
normed_group.of_core ℂ
{ norm_eq_zero_iff := λ z, abs_eq_zero,
  triangle := abs_add,
  norm_neg := abs_neg }

instance : normed_field ℂ :=
{ norm := abs,
  dist_eq := λ _ _, rfl,
  norm_mul' := abs_mul,
  .. complex.field }

instance : nondiscrete_normed_field ℂ :=
{ non_trivial := ⟨2, by simp [norm]; norm_num⟩ }

[Thomas Browning]

so try importing analysis.complex.basic

[Mark Gerads]

Thanks.

[Thomas Browning]

(by the way, the way I found it was by doing a search for nondiscrete_normed_field using the search functionality in VSCode)