pith. machine review for the scientific record. sign in
structure definition def or abbrev

Ledger

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)

  73structure Ledger where
  74  /-- The entries. -/
  75  entries : List LedgerEntry
  76  /-- Double-entry balance: charges sum to zero. -/
  77  balanced : (entries.map LedgerEntry.charge).sum = 0
  78
  79/-! ## C Symmetry: Charge Conjugation from J(x) = J(1/x) -/
  80
  81/-- Apply charge conjugation to a ledger entry. -/

depends on (6)

Lean names referenced from this declaration's body.