Documentation

Lean 4 Proof

theorem damping_cancellation_algebraic {phi_prev sigma_n c_n : ℝ}
    (hsigma : sigma_n ≠ 0) :
    c_n * (phi_prev / sigma_n) * sigma_n = c_n * phi_prev := by
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:60

Module Section

Proposition 6, Theorem 9, Corollaries 1-2 and 4:

In the same file