how do I define cases in a function output?

Stream: new members

[Mark Gerads]

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]

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]

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

[Mark Gerads]

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?

[Johan Commelin]

@Mark Gerads try it with integers instead of complex numbers

[Johan Commelin]

You can't compute with arbitrary complex numbers, and hence Lean can't compute with any complex number

[Mark Gerads]

It works now. Thanks. I suppose I only need for the integers so far anyway.