structure definition def or abbrev

`MainSequenceStar`

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

formal statement (Lean)

 154structure MainSequenceStar where
 155  mass : ℝ
 156  h_pos : 0 < mass
 157

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

hr_diagram_direction in IndisputableMonolith.Physics.StellarEvolution decl_use
ms_luminosity in IndisputableMonolith.Physics.StellarEvolution decl_use
ms_temperature in IndisputableMonolith.Physics.StellarEvolution decl_use