## Stream: new members

### Topic: Repeated derivative of a complex function

#### Mark Gerads (Feb 26 2021 at 05:11):

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 (Feb 26 2021 at 05:25):

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 (Feb 26 2021 at 05:25):

in analysis/complex/basic, I found this:

instance : normed_group ℂ :=
normed_group.of_core ℂ
{ norm_eq_zero_iff := λ z, abs_eq_zero,
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 (Feb 26 2021 at 05:26):

so try importing analysis.complex.basic

Thanks.

#### Thomas Browning (Feb 26 2021 at 05:30):

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

Last updated: May 13 2021 at 20:13 UTC