Documentation

Lean 4 Proof

theorem ngmEntryReal_linear_in_J {beta_n sigma_n J_n Fbar_n sigma_prev alpha : ℝ}
    (hsp : sigma_prev ≠ 0) :
    ngmEntryReal beta_n sigma_n (alpha * J_n) Fbar_n sigma_prev =
    alpha * ngmEntryReal beta_n sigma_n J_n Fbar_n sigma_prev := by
  simp only [ngmEntryReal]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:120

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)

In the same file