kronecker symbol

Stream: maths

[Sebastien Gouezel]

Do we have the kronecker symbol somewhere in mathlib (I mean, δ R i j which is equal to (1 : R) if i = j, and (0 : R) otherwise)?

[Scott Morrison]

Pretty sure not. I was tempted to introduce it once but didn't have the enthusiasm to use it everywhere it could be.

[Sebastien Gouezel]

I am doing some elementary linear algebra with matrices, and it would prove pretty useful there!

[Scott Morrison]

I think it's a great idea.

[Scott Morrison]

If we had square brackets to spare I'd love if we could just write [P] for if P then 1 else 0, and then write [i = j] for the Kronecker delta. Maybe that's too hard notationally.

[Scott Morrison]

But I would happily endorse introducing it somewhere, and leaving it to later to use in the rest of the library.

[Anne Baanen]

It's sometimes spelled using docs#function.update, δ i j = function.update 0 i 1 j

[Scott Morrison]

Terse, but not super readable. :-)

[Eric Rodriguez]

I feel like if anything it could just be notation for ite, because there's enough API there

[Anne Baanen]

Or even docs#pi.single i 1 j, apparently