Documentation

Lean 4 Proof

theorem antisymPart_antisymmetric (A : Fin N → Fin N → ℝ) :
    IsAntisymmetric (antisymPart A) := by
  intro i j; simp only [antisymPart]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:45

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file