Documentation

Lean 4 Proof

theorem symPart_symmetric (A : Fin N → Fin N → ℝ) :
    IsSymmetricMatrix (symPart A) := by
  intro i j; simp only [symPart]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:40

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file