Jacobian Discriminant

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def jacobianDiscriminant (tr det : ℝ) : ℝ := tr ^ 2 - 4 * det

Dependency Graph

Used by

spiral_iff_discriminant_neg cross_coupling_creates_spiral

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:39

Module Section

Coupled (ρ, T) Jacobian Analysis