Documentation

Lean 4 Proof

theorem compound_symmetry_trace (J : ℕ) (s_sq g : ℝ) :
    compoundSymmEigMarket J s_sq g + (↑J - 1) * compoundSymmEigIdio s_sq g =
    ↑J * s_sq := by
  simp only [compoundSymmEigMarket, compoundSymmEigIdio]
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:163

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file