Documentation

Lean 4 Proof

theorem keff_reduced_universal (J : ℕ) (ρ T Tstar : ℝ)
    (hK : curvatureK J ρ ≠ 0) :
    effectiveCurvatureKeff J ρ T Tstar / curvatureK J ρ =
      reducedOrderParam T Tstar := by
  rw [keff_eq_K_times_reduced]
  exact mul_div_cancel_left₀ _ hK

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:268

Module Section

Phase Transition at T* (Gap #8)

In the same file