OAI/Geometry/HeilbronnTriangle/PrimePowerGL.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.PrimePowerGL.map_GL_surjective line 10
  2. theorem OAI.Problem355.PrimePowerGL.prime_power_reflects_units line 30
  3. theorem OAI.Problem355.PrimePowerGL.prime_power_GL_surjective line 42
  4. def OAI.Problem355.PrimePowerGL.fiberEquivKer line 51
  5. def OAI.Problem355.PrimePowerGL.unitsEquivSigmaFiber line 73
  6. theorem OAI.Problem355.PrimePowerGL.card_units_of_surjective line 87
  7. def OAI.Problem355.PrimePowerGL.matrixKernelEquiv line 103
  8. theorem OAI.Problem355.PrimePowerGL.card_matrix_kernel line 116
  9. theorem OAI.Problem355.PrimePowerGL.card_GL_of_surjective line 123
  10. theorem OAI.Problem355.PrimePowerGL.card_prime_power_kernel line 140
  11. theorem OAI.Problem355.PrimePowerGL.card_GL_prime_power line 158
  12. theorem OAI.Problem355.PrimePowerGL.card_GL_three_field line 169
  13. theorem OAI.Problem355.PrimePowerGL.card_GL_three_field_lower line 175
  14. theorem OAI.Problem355.PrimePowerGL.card_GL_three_prime_power_lower line 210