theorem proved term proof

`deriv_constant`

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

formal statement (Lean)

  66theorem deriv_constant (c : ℝ) (μ : Fin 4) (x : Fin 4 → ℝ) :
  67  directional_deriv (constant c) μ x = 0 := by

Term-mode proof.

  68  simp only [directional_deriv, constant]
  69  norm_num
  70
  71/-- Gradient: collection of all directional derivatives ∂_μ ψ. -/

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use
directional_deriv in IndisputableMonolith.Relativity.Fields.Scalar decl_use