Documentation

Lean 4 Proof

def jacobianDet (df_rho_drho df_T_dT df_rho_dT df_T_drho : ℝ) : ℝ :=
  df_rho_drho * df_T_dT - df_rho_dT * df_T_drho

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:33

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file