Documentation

Lean 4 Proof

theorem qFriction_measurement_formula (T Cov Response : ℝ) (hR : Response ≠ 0)
    (hFDT : Response = Cov / T) (hT : T ≠ 0) :
    T = Cov / Response := by
  have h : Response * T = Cov := by
    field_simp at hFDT
    linarith
  field_simp
  linarith

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:66

Module Section

Theorems 5-7, Corollaries 2-4, Propositions 8-11:

In the same file