Lean 4 Proof

theorem antisym_preserves_sum {A : Fin N → Fin N → ℝ}
    (hA : IsAntisymmetric A) :
    ∀ v : Fin N → ℝ, (∀ i, v i = 1) →
    ∑ i, ∑ j, A i j * v j = 0 := by
  intro v hv
  simp_rw [hv, mul_one]
  exact antisym_total_sum_zero hA

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:340

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file