IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D · Recognition explainer

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.ClausiusEinsteinBridge module_import

declarations in this module (118)

abbrev Mat4 L57
def IsSymmetric L59
def raise L63
def minkowskiDot L67
def minkowskiTrace L71
def IsLorentzTraceless L74
def IsLorentzTransverse L78
def IsLorentzTT L82
def minkowskiEta L85
def gaugePart L87
def outerSq L90
def symmetrizedOuter L93
def lorentzLoad L97
theorem lorentzLoad_eq L100
theorem IsLorentzTransverse_iff_lorentzLoad L106
theorem minkowskiDot_eq_sum L112
theorem minkowskiDot_comm L117
theorem minkowskiTrace_eq_sum L121
theorem gaugePart_symmetric L128
theorem outerSq_symmetric L132
theorem symmetrizedOuter_symmetric L136
theorem raise_raise L140
theorem lorentzLoad_smul L147
theorem lorentzLoad_sub L153
theorem lorentzLoad_eta L157
theorem lorentzLoad_outerSq L163
theorem lorentzLoad_symmetrizedOuter L173
theorem lorentzLoad_symmetrizedOuter_l L190
theorem lorentzLoad_gaugePart L207
theorem minkowskiTrace_smul L224
theorem minkowskiTrace_sub L230
theorem minkowskiTrace_add L236
theorem minkowskiTrace_eta L242
theorem minkowskiTrace_outerSq L246
theorem minkowskiTrace_symmetrizedOuter L250
theorem minkowskiDot_eq_MinkowskiNull L254
def transverseProjector L261
def gaugeVector L264
def gaugeCorrected L270
def residualTrace L273
def ttProject L276
theorem minkowskiEta_symmetric L279
theorem transverseProjector_symmetric L286
theorem lorentzLoad_transverseProjector L293
theorem minkowskiDot_gaugeVector L300
theorem lorentzLoad_gaugePart_gaugeVector L348
theorem gaugeCorrected_transverse L363
theorem gaugeCorrected_symmetric L370
theorem minkowskiTrace_transverseProjector L377
theorem ttProject_symmetric L385
theorem ttProject_transverse L393
theorem ttProject_traceless L403
theorem ttProject_isLorentzTT L411
theorem exists_lorentzTTDecomposition L420
theorem exists_lorentzTTDecomposition' L428
def nullProjector L439
def nullSMixed L442
def kron L445
def nullPMixed L447
def nullPhp L451
def nullBilinear L456
def nullMGaugeVector L460
def nullLGaugeVector L463
def nullGap L467
def nullTraceCoeff L472
def nullTTProject L475
theorem nullProjector_symmetric L478
theorem nullProjector_minkowskiTrace L485
theorem lorentzLoad_nullProjector_m L493
theorem lorentzLoad_nullProjector_l L502
theorem sum_kron_left L511
theorem sum_kron_right L520
theorem nullPhp_expand_algebra L529
theorem sum_kron_H_kron L549
theorem sum_S_H_kron L561
theorem sum_kron_H_S L571
theorem nullPhp_entry L582
theorem sum_nullSMixed_H_col L592
theorem sum_H_nullSMixed_row L612
theorem nullGap_entry L628

… and 38 more