Documentation

Lean 4 Proof

def acrGainsFromTrade (lam ρ : ℝ) : ℝ :=
  lam ^ (-(1 / ρ - 1))

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:309

Module Section

Economics extensions for CES formalization:

In the same file