`kronecker_off_diag`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.Manifold
domain: Relativity
line: 77 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.Geometry.Manifold on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  74  kronecker μ μ = 1 := by
  75  simp [kronecker]
  76
  77theorem kronecker_off_diag {n : ℕ} (μ ν : Fin n) (h : μ ≠ ν) :
  78  kronecker μ ν = 0 := by
  79  simp [kronecker, h]
  80
  81/-- Partial derivative of a scalar function using a directional derivative along the basis vector. -/
  82noncomputable def partialDeriv {M : Manifold} (f : Point M → ℝ) (μ : Fin M.dim) (x : Point M) : ℝ :=
  83  deriv (fun t => f (fun i => if i = μ then x i + t else x i)) 0
  84
  85
  86end Geometry
  87end Relativity
  88end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.