Documentation

Lean 4 Proof

theorem tradeCoupling_antisymmetric (a : Fin N → Fin N → ℝ) :
    IsAntisymmetric (tradeCouplingMatrix a) := by
  intro i j; simp only [tradeCouplingMatrix]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/Defs.lean:175

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file