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)
172noncomputable def logChargeAsNoether (N : ℕ) : NoetherCharge N where
173 value := log_charge
proof body
Definition body.
174 conserved := fun _ _ h => h.1
175
176/-- Every topological charge induces a Noether charge by ℤ ↪ ℝ. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
NoetherCharge
in IndisputableMonolith.Foundation.TopologicalConservation
decl_use
-
log_charge
in IndisputableMonolith.Foundation.VariationalDynamics
decl_use
-
NoetherCharge
in IndisputableMonolith.QFT.NoetherTheorem
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use