No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
62def kronecker {n : ℕ} (μ ν : Fin n) : ℝ := if μ = ν then 1 else 0
proof body
Definition body.
63
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.
-
kronecker_diag
in IndisputableMonolith.Relativity.Geometry.Manifold
decl_use
-
kronecker_off_diag
in IndisputableMonolith.Relativity.Geometry.Manifold
decl_use
-
kronecker_symm
in IndisputableMonolith.Relativity.Geometry.Manifold
decl_use
-
inverse_1PN_correct
in IndisputableMonolith.Relativity.PostNewtonian.Metric1PN
decl_use
-
PPNInverseFacts
in IndisputableMonolith.Relativity.PostNewtonian.Metric1PN
decl_use