theorem proved wrapper

`kronecker_diag`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  73theorem kronecker_diag {n : ℕ} (μ : Fin n) :
  74  kronecker μ μ = 1 := by

One-line wrapper that applies simp.

  75  simp [kronecker]
  76

Lean names referenced from this declaration's body.