theorem proved wrapper

`alphaInv_pos`

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

formal statement (Lean)

  55private theorem alphaInv_pos : 0 < alphaInv := by

One-line wrapper that applies linarith.

  56  linarith [alphaInv_gt]
  57

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

row_hartree_over_rest_eq in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_hartree_over_rest_lower in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_hartree_over_rest_upper in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_eq in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_lower in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_upper in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
ae_den_pos in IndisputableMonolith.Physics.ElectronGMinus2ScoreCard decl_use
alphaInv_pos in IndisputableMonolith.Physics.ElectronGMinus2ScoreCard decl_use
row_electron_ae_leading_eq in IndisputableMonolith.Physics.ElectronGMinus2ScoreCard decl_use
row_electron_ae_leading_lower in IndisputableMonolith.Physics.ElectronGMinus2ScoreCard decl_use

Lean names referenced from this declaration's body.

alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alphaInv_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alphaInv_pos in IndisputableMonolith.Physics.ElectronGMinus2ScoreCard decl_use