Documentation

Lean 4 Proof

theorem settlementR0_friction_one (e : SettlementEconomy) :
    settlementR0_friction e 1 = settlementR0 e := by
  rw [settlementR0_friction_eq]; ring

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:126

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file