OAI/GroupTheory/SimpleAmenable/Homology/ArithmeticTangentBasis.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.cutRing_coefficients line 14
  2. theorem OAI.SimpleAmenable.cutTau_inverse_mul line 18
  3. theorem OAI.SimpleAmenable.cutRing_coefficients_bound line 23
  4. theorem OAI.SimpleAmenable.tangent_basis_coefficients line 47
  5. theorem OAI.SimpleAmenable.exists_short_tangent_basis line 70
  6. def OAI.SimpleAmenable.integerSteps line 90
  7. theorem OAI.SimpleAmenable.integerSteps_sum line 93
  8. theorem OAI.SimpleAmenable.integerSteps_length line 104
  9. theorem OAI.SimpleAmenable.integerSteps_mem line 113
  10. theorem OAI.SimpleAmenable.sum_abs_bound_by_length line 121
  11. theorem OAI.SimpleAmenable.endpointLabel_list_sum line 135
  12. theorem OAI.SimpleAmenable.tangent_chain line 142