Documentation

Lean 4 Proof

theorem spiral_iff_discriminant_neg {tr det : ℝ} :
    jacobianDiscriminant tr det < 0 ↔ tr ^ 2 < 4 * det := by
  simp only [jacobianDiscriminant]; constructor <;> intro h <;> linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:88

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file