theorem
proved
kronecker_diag
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geometry.Manifold on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
70 exact h hνμ.symm
71 simp [kronecker, h, h']
72
73theorem kronecker_diag {n : ℕ} (μ : Fin n) :
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