Documentation

Lean 4 Proof

theorem settlementR0Friction_eq (e : SettlementEconomy) (lambda_B : ℝ) :
    settlementR0Friction e lambda_B = lambda_B * settlementR0 e := by
  simp only [settlementR0Friction, settlementR0]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:120

Module Section

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

In the same file