Documentation

Lean 4 Proof

theorem crossingTemperature_pos {DeltaPhi DeltaS_q : ℝ}
    (hPhi : 0 < DeltaPhi) (hS : 0 < DeltaS_q) :
    0 < crossingTemperature DeltaPhi DeltaS_q := by
  exact div_pos hPhi hS

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:233

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file