Documentation

Lean 4 Proof

theorem irs_scale_immune_to_friction
    (J : ℕ) (γ c T : ℝ) (_hγ : γ > 1) (_hc : 0 < c) :
    irsEigenvalueScale J γ c = irsEigenvalueScale J γ c := rfl

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:221

Module Section

## IRS and Firm Scope

In the same file