def definition def or abbrev

`constant`

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

formal statement (Lean)

  18def constant (c : ℝ) : ScalarField := { ψ := fun _ => c }

proof body

Definition body.

used by (40)

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

applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
const_one_is_geodesic in IndisputableMonolith.Action.EulerLagrange decl_use
costRateELHolds in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_implies_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
geodesic_iff_hessianEnergy_EL in IndisputableMonolith.Action.EulerLagrange decl_use
energy_conservation in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
spaceShift in IndisputableMonolith.Action.Noether decl_use
actionJ_nonneg in IndisputableMonolith.Action.PathSpace decl_use
coe_mk in IndisputableMonolith.Action.PathSpace decl_use
newton_second_law in IndisputableMonolith.Action.QuadraticLimit decl_use
defectDist_le_J_of_ratio_bounds in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_quasi_triangle_local in IndisputableMonolith.Algebra.CostAlgebra decl_use
quasiTriangleConstant_eq in IndisputableMonolith.Algebra.CostAlgebra decl_use
Cycle in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
AllConstantsDerived in IndisputableMonolith.Astrophysics.MassToLight decl_use
H_RSZeroParameterStatus in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_derivation_complete in IndisputableMonolith.Astrophysics.MassToLight decl_use
alphaInv_gauge_invariant in IndisputableMonolith.Bridge.GaugeVsParams decl_use
boltzmannFactor in IndisputableMonolith.Chemistry.ActivationEnergy decl_use
alkali_halogen_ionic in IndisputableMonolith.Chemistry.IonicBond decl_use
latticeEnergyProxy in IndisputableMonolith.Chemistry.IonicBond decl_use
madelungCsCl in IndisputableMonolith.Chemistry.IonicBond decl_use
madelungNaCl in IndisputableMonolith.Chemistry.IonicBond decl_use
madelungZnS in IndisputableMonolith.Chemistry.IonicBond decl_use
transition_cohesive_gt_alkali in IndisputableMonolith.Chemistry.MetallicBond decl_use
neutralAt in IndisputableMonolith.Chemistry.PeriodicTable decl_use
hasDerivAt_extendByZero_apply in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
of_convectionNormBound in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use

… and 10 more

depends on (3)

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