# Zulip Chat Archive

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

so try importing `analysis.complex.basic`

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

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