Documentation

Lean 4 Proof

theorem io_decomposition (A : Fin N → Fin N → ℝ) (i j : Fin N) :
    A i j = symPart A i j + antisymPart A i j := by
  simp only [symPart, antisymPart]
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:34

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file