def definition def or abbrev

`zeroCharge`

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

formal statement (Lean)

  94def zeroCharge (N : ℕ) : TopologicalCharge N where
  95  value := fun _ => 0

Definition body.

  96  conserved := fun _ _ _ => rfl
  97
  98/-- A constant topological charge. -/

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
TopologicalCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
TopologicalCharge in IndisputableMonolith.Physics.TopologicalChargesFromConfigDim decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use