IndisputableMonolith.Cosmology.SIConversion

declarations in this module (22)

• def planck_length_SI L47
• def planck_time_SI L51
• def c_SI L54
• def Mpc_SI L58
• def ly_SI L61
• def Gyr_SI L64
• theorem planck_length_SI_pos L66
• theorem planck_time_SI_pos L69
• theorem c_SI_pos L72
• theorem Mpc_SI_pos L75
• def planck_to_meters L81
• def planck_to_seconds L84
• def hubble_to_kms_mpc L88
• def seconds_to_Gyr L92
• def meters_to_Gly L95
• def obs_radius_m L102
• def obs_age_s L106
• def obs_age_Gyr L109
• def obs_H0_early L113
• def obs_H0_late L117
• structure SICalibrationCert L121
• theorem si_calibration_cert L127