No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
24abbrev Vec3 := ℝ × ℝ × ℝ
proof body
Definition body.
25
26/-- Placeholder thrust observable on a medium state.
27
28This will be refined to a pressure-gradient / control-volume expression.
29-/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
Trace
in IndisputableMonolith.Flight.Falsifiers
decl_use
-
netThrust
in IndisputableMonolith.Flight.Thrust
decl_use
-
thrustVector
in IndisputableMonolith.Flight.Thrust
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
pressure
in IndisputableMonolith.ILG.PressureForm
decl_use
-
volume
in IndisputableMonolith.Papers.GCIC.BrainHolography
decl_use
-
gradient
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use