Documentation

Lean 4 Proof

theorem antisym_total_sum_zero {A : Fin N → Fin N → ℝ}
    (hA : IsAntisymmetric A) :
    ∑ i, ∑ j, A i j = 0 := by
  have key : ∀ i j : Fin N, A i j = -A j i := hA
  have h : ∑ i, ∑ j, A i j = -(∑ i, ∑ j, A i j) := by
    conv_lhs =>
      rw [Finset.sum_comm]
      arg 2; ext y; arg 2; ext x
      rw [key x y]
    simp only [Finset.sum_neg_distrib]
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:328

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file