Documentation

Lean 4 Proof

theorem premium_over_linear_factor {ρ : ℝ} (hρ : ρ ≠ 0) :
    1 / ρ - 1 = (1 - ρ) / ρ := by field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:847

Module Section

## Network Scaling Results

In the same file