OAI/Analysis/Commutator/FreeActionUnitary.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.FreeWordAction.action_invline 35 - def
OAI.Kadison.FreeWordAction.equivline 43 - lemma
OAI.Kadison.FreeWordAction.equiv_applyline 55 - def
OAI.Kadison.FreeWordAction.representationline 59 - lemma
OAI.Kadison.FreeWordAction.representation_applyline 74 - lemma
OAI.Kadison.FreeWordAction.representation_continuousline 78