theorem proved tactic proof

`kronecker_symm`

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

formal statement (Lean)

  64theorem kronecker_symm {n : ℕ} (μ ν : Fin n) :
  65  kronecker μ ν = kronecker ν μ := by

proof body

Tactic-mode proof.

  66  by_cases h : μ = ν
  67  · simp [kronecker, h]
  68  · have h' : ν ≠ μ := by
  69      intro hνμ
  70      exact h hνμ.symm
  71    simp [kronecker, h, h']
  72

depends on (1)

Lean names referenced from this declaration's body.

kronecker in IndisputableMonolith.Relativity.Geometry.Manifold decl_use