Documentation

Lean 4 Proof

def jacobian3DTrace (a_ρρ a_TT a_JJ : ℝ) : ℝ :=
  a_ρρ + a_TT + a_JJ

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:90

Module Section

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

In the same file