Documentation Verification Report

SelfAdjoint

πŸ“ Source: PhysLean/Relativity/SL2C/SelfAdjoint.lean

Statistics

MetricCount
DefinitionstoSelfAdjointEquiv, toSelfAdjointMap', Β«termβ„‚Β²Λ£Β²Β», ℍ₂
4
TheoremstoSelfAdjointMap_det_one', toSelfAdjointMap_mul, toSelfAdjointMap_similar_det
3
Total7

Lorentz

Definitions

NameCategoryTheorems
Β«termβ„‚Β²Λ£Β²Β» πŸ“–CompOpβ€”
ℍ₂ πŸ“–CompOp
3 mathmath: SL2C.toSelfAdjointMap_det_one', SL2C.toSelfAdjointMap_similar_det, SL2C.toSelfAdjointMap_mul

Lorentz.SL2C

Definitions

NameCategoryTheorems
toSelfAdjointEquiv πŸ“–CompOpβ€”
toSelfAdjointMap' πŸ“–CompOp
3 mathmath: toSelfAdjointMap_det_one', toSelfAdjointMap_similar_det, toSelfAdjointMap_mul

Theorems

NameKindAssumesProvesValidatesDepends On
toSelfAdjointMap_det_one' πŸ“–mathematicalMatrix.IsUpperTriangularLorentz.ℍ₂
toSelfAdjointMap'		β€”β€”
toSelfAdjointMap_mul πŸ“–mathematicalβ€”toSelfAdjointMap'
Lorentz.ℍ₂		β€”β€”
toSelfAdjointMap_similar_det πŸ“–mathematicalβ€”Lorentz.ℍ₂
toSelfAdjointMap'		β€”toSelfAdjointMap_mul

---

← Back to Index