theorem proved term proof

`differentiableAt_coordRay_i_sq`

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

formal statement (Lean)

 360theorem differentiableAt_coordRay_i_sq (x : Fin 4 → ℝ) (μ i : Fin 4) :
 361    DifferentiableAt ℝ (fun t => (coordRay x μ t) i ^ 2) 0 := by

Term-mode proof.

 362  apply DifferentiableAt.pow (differentiableAt_coordRay_i x μ i) 2
 363
 364/-- Closed form for ∂μ (xᵢ²). -/

From the project-wide theorem graph. These declarations reference this one in their body.

differentiableAt_coordRay_spatialNormSq in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
pow in IndisputableMonolith.RecogSpec.Core decl_use
coordRay in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
differentiableAt_coordRay_i in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use