IndisputableMonolith.Relativity.Cosmology.FRWFriedmann

declarations in this module (33)

• def gMetric L49
• def gInv L53
• def pd L58
• def RicciT L70
• def RicciScalarT L78
• def EinsteinT L82
• def Tmn L90
• def EinsteinEqns L100
• lemma deriv_a_sq L107
• lemma gMetric_00 L114
• lemma gMetric_spatial L118
• lemma gMetric_offdiag L123
• lemma christoffel_0_00 L128
• theorem christoffel_0_11 L133
• theorem christoffel_0_22 L140
• theorem christoffel_0_33 L147
• theorem christoffel_1_01 L154
• theorem christoffel_2_02 L163
• theorem christoffel_3_03 L172
• theorem christoffel_symm L182
• theorem deriv_hubble L199
• theorem deriv_a_adot L211
• theorem ricci_00 L223
• lemma christoffel_1_10 L237
• theorem ricci_11 L243
• lemma ricci_22 L256
• lemma ricci_33 L269
• theorem ricci_scalar_eq L282
• theorem einstein_00 L295
• theorem einstein_11 L306
• theorem friedmann_I L320
• theorem friedmann_II L330
• theorem friedmannCert L357