lemma proved wrapper

`phi_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)

  68lemma phi_zero_of_balanced {M} (L : Ledger M) (hbal : ∀ u, L.debit u = L.credit u) :
  69  ∀ u, phi L u = 0 := by

One-line wrapper that applies intro.

  70  intro u; simp [phi, hbal u, sub_self]
  71

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

Lean names referenced from this declaration's body.