def definition def or abbrev

`smul`

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

formal statement (Lean)

  33def smul (c : ℝ) (φ : ScalarField) : ScalarField :=

Definition body.

  34  { ψ := fun x => c * φ.ψ x }
  35

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

Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
duhamelKernelDominatedConvergenceAt_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
duhamelRemainderOfGalerkin_integratingFactor in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
duhamelRemainderOfGalerkin_kernel in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall_kernelIntegral_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
deriv_smul in IndisputableMonolith.Relativity.Fields.Scalar decl_use
smul_zero in IndisputableMonolith.Relativity.Fields.Scalar decl_use
strictConcaveOn_gapR_Ici in IndisputableMonolith.RSBridge.GapProperties decl_use

Lean names referenced from this declaration's body.

ScalarField in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
ScalarField in IndisputableMonolith.Relativity.Fields.Scalar decl_use
ScalarField in IndisputableMonolith.Relativity.Geometry.Tensor decl_use