lemma proved wrapper

`chainFlux_zero_of_balanced`

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

formal statement (Lean)

  72lemma chainFlux_zero_of_balanced {M} (L : Ledger M) (ch : Chain M)
  73  (hbal : ∀ u, L.debit u = L.credit u) :
  74  chainFlux L ch = 0 := by

One-line wrapper that applies simp.

  75  simp [chainFlux, phi_zero_of_balanced (M:=M) L hbal]
  76

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

twoStep in IndisputableMonolith.Recognition decl_use
chainFlux_zero_of_balanced in IndisputableMonolith.RRF.Core.Recognition decl_use

Lean names referenced from this declaration's body.

Chain in IndisputableMonolith.Chain decl_use
chainFlux in IndisputableMonolith.Chain decl_use
Chain in IndisputableMonolith.Recognition decl_use
chainFlux in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
phi_zero_of_balanced in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
Chain in IndisputableMonolith.RRF.Core.Recognition decl_use
chainFlux in IndisputableMonolith.RRF.Core.Recognition decl_use
chainFlux_zero_of_balanced in IndisputableMonolith.RRF.Core.Recognition decl_use