## Stream: new members

### Topic: how do I define cases in a function output?

#### Mark Gerads (Mar 01 2021 at 08:26):

I want to define the https://www.wikiwand.com/en/Kronecker_delta on the complex numbers: it is the function which maps 0 to 1 and everything else to 0. I want it in the form def kron_del (z : ℂ) : ℂ :=, but a more general form in Mathlib might be good. Please help. :). I need it for my pet formalization project.

#### Jakob Scholbach (Mar 01 2021 at 08:40):

Looking at https://leanprover.github.io/introduction_to_lean/introduction_to_lean.pdf, specifically p. 29 there: you might want to try an if ... then ... else.

#### Eric Wieser (Mar 01 2021 at 08:40):

pi.single 0 1 z? (docs#pi.single)

#### Mark Gerads (Mar 01 2021 at 08:50):

def kron_del (z : ℂ) : ℂ := if z = 0 then 1 else 0
#eval kron_del 0


results in

code generation failed, VM does not have code for 'classical.dec_eq'


This is the first time I have seen this error.

def kron_del (z : ℂ) : ℂ := pi.single 0 1 z
#eval kron_del 0


results in the same error. Maybe #eval is what is broken?