module
module
IndisputableMonolith.Physics.StellarEvolution
show as:
view Lean formalization →
depends on (1)
declarations in this module (21)
-
def
nuclear_efficiency -
theorem
nuclear_efficiency_valid -
def
gamow_energy -
theorem
gamow_energy_increases_with_T -
def
virial_temperature -
theorem
temp_increases_with_mass -
def
main_sequence_radius -
theorem
radius_sublinear -
def
luminosity_scaling -
theorem
luminosity_increases -
theorem
solar_calibration -
theorem
massive_star_more_luminous -
def
ms_lifetime -
theorem
lifetime_decreases -
theorem
solar_lifetime_approx -
def
chandrasekhar_limit -
theorem
endpoint_classification -
structure
MainSequenceStar -
def
ms_luminosity -
def
ms_temperature -
theorem
hr_diagram_direction