lemma proved term proof

`coordRay_coordRay`

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

formal statement (Lean)

  29@[simp] lemma coordRay_coordRay (x : Fin 4 → ℝ) (μ : Fin 4) (s t : ℝ) :
  30    coordRay (coordRay x μ s) μ t = coordRay x μ (s + t) := by

Term-mode proof.

  31  funext ν; simp [coordRay]; ring
  32
  33/-- Directional derivative `∂_μ f(x)` via real derivative along the coordinate ray. -/

Lean names referenced from this declaration's body.