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)
70structure MediumStateH where
71 S : MediumState
72 H : HelicityProxy
73
74end Medium
75end Flight
76end IndisputableMonolith
77
depends on (6)
Lean names referenced from this declaration's body.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
HelicityProxy
in IndisputableMonolith.Flight.Medium
decl_use
-
MediumState
in IndisputableMonolith.Flight.Medium
decl_use
-
Medium
in IndisputableMonolith.MaxwellDEC
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use