Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:120

Module Section

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

In the same file