Documentation

Lean 4 Proof

theorem common_policy_zero_friction {T_h T_f : ℝ}
    (h : T_h = T_f) :
    monetaryDivergenceFriction T_h T_f = 0 := by
  simp only [monetaryDivergenceFriction, h, sub_self, abs_zero]

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:76

Module Section

Open Economy Monetary Transmission

In the same file