def definition def or abbrev

`ms_temperature`

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

formal statement (Lean)

 159noncomputable def ms_temperature (s : MainSequenceStar) : ℝ := s.mass ^ (0.55 : ℝ)

Definition body.

 160
 161/-- More massive stars are hotter AND more luminous (upper left to lower right in HR). -/

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

hr_diagram_direction in IndisputableMonolith.Physics.StellarEvolution decl_use

Lean names referenced from this declaration's body.