def definition def or abbrev

`rsAlphaFactor`

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

formal statement (Lean)

  24noncomputable def rsAlphaFactor : ℝ := 44 * Real.pi

Definition body.

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

alpha_rung_factor in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
FineStructureCert in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
rsAlphaFactor_gt_100 in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use
rsAlphaFactor_pos in IndisputableMonolith.Physics.FineStructureConstantFromRS decl_use