Documentation

Lean 4 Proof

private lemma rpow_succ_pred {x : ℝ} (hx : 0 < x) (ρ : ℝ) :
    x * x ^ (ρ - 1) = x ^ ρ := by
  have h := rpow_add hx 1 (ρ - 1)
  rw [rpow_one, show 1 + (ρ - 1) = ρ from by ring] at h
  exact h.symm

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:129

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file