definition. Kronecker delta [wiki2024dirac] [uts-0002]
definition. Kronecker delta [wiki2024dirac] [uts-0002]
Kronecker delta \[\delta _{i j}= \begin {cases}0 & \text { if } i \neq j \\ 1 & \text { if } i=j\end {cases}\] or with use of Iverson bracket: \[ \delta _{i j}=[i=j] . \] where \([P]\) is defined as: \[ [P]=\begin {cases}1 & \text { if } P \text { is true } \\ 0 & \text { if } P \text { is false }\end {cases} \]
In Lean 4, the Kronecker delta could be defined as:
def δ (i j : I) : R := (Pi.single i 1 : _ → R) j