Documentation

Lean 4 Proof

def firmContribution (a x ρ : ℝ) : ℝ := a * x ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:27

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file