Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
-- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kronecker.20symbol
import Mathlib.Algebra.Group.Pi.Basic

variable (I : Type*) [DecidableEq I] (R : Type*) [Zero R] [One R]

def kronecker_delta (i j : I) : R := (Pi.single i 1 : _ → R) j