def definition def or abbrev

`radialInv`

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

formal statement (Lean)

 346noncomputable def radialInv (n : ℕ) (x : Fin 4 → ℝ) : ℝ :=

Definition body.

 347  1 / (spatialRadius x) ^ n
 348
 349/-- Differentiability of a coordinate ray component. -/

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

differentiableAt_coordRay_partialDeriv_v2_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
differentiableAt_coordRay_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
differentiableAt_coordRay_spatialRadius in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_radialInv_n in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
laplacian_radialInv_zero_no_const in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_spatialRadius in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
secondDeriv_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
C2DischargeCert in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
differentiableAt_coordRay_partialDeriv_v2_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
laplacian_radialInv_n_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
laplacian_radialInv_zero_no_const_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
partialDeriv_v2_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
secondDeriv_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers 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
spatialRadius in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use