OAI/Analysis/Commutator/UnitaryHaar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.UnitaryHaar.compactUnitary line 17
2. def OAI.Kadison.UnitaryHaar.whole line 28
3. def OAI.Kadison.UnitaryHaar.probability line 33
4. instance OAI.Kadison.UnitaryHaar.(instance at line 35) line 35
5. instance OAI.Kadison.UnitaryHaar.(instance at line 38) line 38