IndisputableMonolith.Gravity.NullConeQuadraticTensorClass

declarations in this module (27)

• def symmetrize4 L50
• theorem symmetrize4_symmetric L53
• theorem symmetrize4_of_symmetric L59
• def antisymmetrize4 L68
• lemma sum_fin_four L72
• theorem quadContr_eq_quadContr_symmetrize4 L80
• theorem quadContr_antisymmetrize4_eq_zero L86
• theorem quadContr_neg L111
• theorem all_null_quad_eq_of_future_nonzero_null_quad_eq L125
• theorem quadContr_smul L164
• theorem quadContr_smul_eta L180
• theorem quadContr_smul_eta_of_null L186
• theorem symmetric_null_zero_eq_scalar_eta_components L201
• theorem null_quadratic_eq_implies_diff_scalar_eta L216
• theorem future_null_quadratic_eq_implies_diff_scalar_eta L236
• theorem diff_scalar_eta_implies_null_quadratic_eq L248
• theorem null_quadratic_eq_iff_diff_scalar_eta L268
• theorem null_quadratic_eq_iff_symmetrize_diff_scalar_eta L286
• def NullConeEquivalent L318
• def DeterminesAlgebraicNullQuadraticClass L347
• theorem determinesAlgebraicNullQuadraticClass_quadContr L358
• theorem determinesAlgebraicNullQuadraticClass_add_eta L369
• def fixedStressFlux L410
• theorem fixedSymmetricStress_determinesAlgebraicNullQuadraticClass L421
• theorem fixedSymmetricStress_null_class_unique L427
• structure NullConeQuadraticTensorClassCert L456
• theorem nullConeQuadraticTensorClassCert L484