Documentation

Lean 4 Proof

theorem acr_gains_autarky (ρ : ℝ) :
    acrGainsFromTrade 1 ρ = 1 := by
  simp only [acrGainsFromTrade]
  exact one_rpow _

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:325

Module Section

Economics extensions for CES formalization:

In the same file