def
definition
twoStep
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Recognition on GitHub at line 105.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
102
103def L : Ledger M := { debit := fun _ => 1, credit := fun _ => 1 }
104
105def twoStep : Chain M :=
106 { n := 1
107 , f := fun _ => ⟨()⟩
108 , ok := by intro i; trivial }
109
110example : chainFlux L twoStep = 0 := by
111 have hbal : ∀ u, L.debit u = L.credit u := by intro _; rfl
112 simpa [chainFlux_zero_of_balanced (M:=M) L twoStep hbal]
113
114end Demo
115
116-- Moved advanced Recognition sections (ClassicalBridge, Potential uniqueness) to Recognition/WIP.lean during modularization.