def definition def or abbrev

`verify_ns`

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

formal statement (Lean)

  15def verify_ns : Prop :=

Definition body.

  16  ∀ m ∈ import_measurements, m.name = "n_s" → |ns_from_inflation Constants.phi - m.value| ≤ m.error
  17

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.