Documentation

Lean 4 Proof

theorem compound_symmetry_decomp (J : ℕ) (s_sq g : ℝ) (i j : Fin J) :
    compoundSymmetryMatrix J s_sq g i j =
    (s_sq - g) * (if i = j then 1 else 0) + g := by
  simp only [compoundSymmetryMatrix]
  split <;> ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:93

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file