OAI/GroupTheory/Thompson/UnitBall.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThompsonNonamenability.UnitBall line 9
2. def OAI.ThompsonNonamenability.unitBallZero line 11
3. theorem OAI.ThompsonNonamenability.coe_unitBallZero line 14
4. theorem OAI.ThompsonNonamenability.unitBall_norm_le line 17