OAI/Analysis/Pureness/GroupAlgebra/FreeGroupFiniteRadial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.freeGroupFiniteBall line 18
2. lemma OAI.CuntzPureness.mem_freeGroupFiniteBall line 21
3. lemma OAI.CuntzPureness.spatialRadialTruncation_generator line 31
4. lemma OAI.CuntzPureness.finiteRadial_eq_truncation_restriction line 46
5. theorem OAI.CuntzPureness.finiteRadial_norm_le line 96