theorem proved term proof

`etaBAt_zero`

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

formal statement (Lean)

  41theorem etaBAt_zero : etaBAt 0 = 1 := by

Term-mode proof.

  42  unfold etaBAt
  43  simp
  44
  45/-- One e-fold cuts η_B by exactly 1/φ. -/

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

baryogenesisTrajectoryCert in IndisputableMonolith.Cosmology.BaryogenesisTrajectory decl_use

Lean names referenced from this declaration's body.