Lean 4 Proof

theorem barrier_vanishes_at_Tcross {DeltaPhi DeltaS_q : ℝ}
    (hS : DeltaS_q ≠ 0) :
    DeltaPhi - crossingTemperature DeltaPhi DeltaS_q * DeltaS_q = 0 := by
  simp only [crossingTemperature]
  rw [div_mul_cancel₀ DeltaPhi hS, sub_self]

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:225

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file