pith. machine review for the scientific record. sign in
theorem proved term proof

noether_core

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 111theorem noether_core {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
 112    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
 113    IsConservedAlong J G.flow := by

proof body

Term-mode proof.

 114  intro x t₁ t₂
 115  rw [hinv t₁ x, hinv t₂ x]
 116
 117/-- The Noether charge is any function conserved by the flow. -/

used by (9)

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

depends on (11)

Lean names referenced from this declaration's body.