def definition def or abbrev

`IsConservedAlong`

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

formal statement (Lean)

  74def IsConservedAlong {X : Type*} (Q : X → ℝ) (φ : ℝ → X → X) : Prop :=

Definition body.

  75  ∀ (x : X) (t₁ t₂ : ℝ), Q (φ t₁ x) = Q (φ t₂ x)
  76
  77/-- Alternative: Q is conserved if Q ∘ φ t = Q for all t. -/

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

space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
time_translation_invariance_implies_energy_conservation in IndisputableMonolith.Action.Noether decl_use
conserved_iff_conserved' in IndisputableMonolith.QFT.NoetherTheorem decl_use
NoetherCharge in IndisputableMonolith.QFT.NoetherTheorem decl_use
noether_core in IndisputableMonolith.QFT.NoetherTheorem decl_use
noether_summary in IndisputableMonolith.QFT.NoetherTheorem decl_use
phase_invariance_implies_conservation in IndisputableMonolith.QFT.NoetherTheorem decl_use
space_invariance_implies_conservation in IndisputableMonolith.QFT.NoetherTheorem decl_use
time_invariance_implies_conservation in IndisputableMonolith.QFT.NoetherTheorem decl_use

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use