def
scaffolding
sorry stub
noether_status
show as:
view Lean formalization →
formal statement (Lean)
124def noether_status : String :=
proof body
Body contains sorry. Scaffold only; not proved.
125 "Action.Noether: time/space translation invariance ⇒ Noether conservation, energy_conservation_of_J_action (0 sorry, 0 axiom)"
126
127end Noether
128end Action
129end IndisputableMonolith