Documentation

Lean 4 Proof

theorem specific_heat_zero_at_symmetry [NeZero J]
    {c₀ : ℝ} (hc : 0 < c₀) (ρ : ℝ) :
    specificHeat (fun _ : Fin J => c₀) ρ = 0 := by
  unfold specificHeat
  rw [escort_fisher_zero_at_symmetry hc ρ, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:235

Module Section

### The Thermodynamic Decomposition of Value

In the same file