def definition def or abbrev

`netThrust`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  36noncomputable def netThrust (f : ℕ → Vec3) (t0 N : ℕ) : Vec3 :=

proof body

Definition body.

  37  ( (Finset.range N).sum (fun k => (f (t0 + k)).1)
  38  , (Finset.range N).sum (fun k => (f (t0 + k)).2.1)
  39  , (Finset.range N).sum (fun k => (f (t0 + k)).2.2) )
  40
  41end Thrust
  42end Flight
  43end IndisputableMonolith
  44

depends on (1)

Lean names referenced from this declaration's body.

Vec3 in IndisputableMonolith.Flight.Thrust decl_use