Documentation

Lean 4 Proof

theorem debtDynamics_eq_zero_iff {r_B g b d : ℝ} :
    debtDynamics r_B g b d = 0 ↔ d = (g - r_B) * b := by
  simp only [debtDynamics]; constructor <;> intro h <;> linarith

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:358

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file