IndisputableMonolith.Gravity.HawkingTemperatureSI

declarations in this module (25)

• def k_B_SI L117
• theorem k_B_SI_pos L119
• def T_hawking_SI L126
• theorem T_hawking_SI_def L129
• theorem hawking_temperature_SI L135
• theorem T_hawking_SI_pos L140
• theorem T_hawking_SI_strict_anti L151
• theorem T_hawking_SI_eq_geom_via_bridge L185
• theorem T_hawking_geom_eq_SI_via_bridge L198
• def schwarzschildRadius_SI L220
• theorem schwarzschildRadius_SI_def L223
• theorem schwarzschildRadius_SI_pos L226
• theorem T_hawking_SI_eq_inv_schwarzschildRadius L241
• def t_Page_SI L281
• theorem t_Page_SI_def L284
• def K_Page_SI L290
• theorem K_Page_SI_pos L293
• theorem t_Page_SI_eq_K_mul_M_cube L306
• theorem t_Page_SI_pos L314
• theorem t_Page_SI_strict_mono L319
• theorem t_Page_SI_squared_planck_form L334
• structure HawkingTemperatureSICert L350
• def hawkingTemperatureSICert L385
• theorem hawkingTemperatureSICert_inhabited L400
• theorem hawking_temperature_SI_one_statement L411