OAI/Analysis/Commutator/DihedralHaar.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.DihedralCorner.wave_natline 28 - lemma
OAI.Kadison.DihedralCorner.wave_positive_traceline 32 - lemma
OAI.Kadison.DihedralCorner.wave_trace_zeroline 40 - lemma
OAI.Kadison.DihedralCorner.wave_traceline 51 - theorem
OAI.Kadison.DihedralCorner.dihedral_haarline 57 - lemma
OAI.Kadison.DihedralCorner.reflection_positive_traceline 65 - lemma
OAI.Kadison.DihedralCorner.symmetry_starline 76 - lemma
OAI.Kadison.DihedralCorner.reflection_traceline 81