OAI/GroupTheory/PeriodicGroups/Homology/KernelStability.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Stability.RationalKernel.J line 15
  2. abbrev OAI.SourceBurnside.Stability.RationalKernel.step line 16
  3. def OAI.SourceBurnside.Stability.RationalKernel.kernelStep line 21
  4. lemma OAI.SourceBurnside.Stability.RationalKernel.central line 32
  5. def OAI.SourceBurnside.Stability.RationalKernel.liftKernel line 39
  6. def OAI.SourceBurnside.Stability.RationalKernel.character line 46
  7. lemma OAI.SourceBurnside.Stability.RationalKernel.inl_character line 47
  8. theorem OAI.SourceBurnside.Stability.RationalKernel.restriction_surjective line 52
  9. def OAI.SourceBurnside.Stability.SurjectiveDescent.descend line 103
  10. lemma OAI.SourceBurnside.Stability.SurjectiveDescent.descend_apply line 106
  11. lemma OAI.SourceBurnside.Stability.RationalBar.coboundary_of_lift line 117
  12. lemma OAI.SourceBurnside.Stability.RationalBar.coboundary_value_eq line 141
  13. def OAI.SourceBurnside.Stability.RationalBar.liftOfCoboundary line 148
  14. lemma OAI.SourceBurnside.Stability.RationalBar.liftOfCoboundary_projection line 161
  15. lemma OAI.SourceBurnside.Stability.RationalBar.pull_id line 164
  16. def OAI.SourceBurnside.Stability.RationalKernel.restriction line 183
  17. lemma OAI.SourceBurnside.Stability.RationalKernel.restriction_eq_one line 188
  18. lemma OAI.SourceBurnside.Stability.RationalKernel.restriction_injective line 235
  19. def OAI.SourceBurnside.Stability.RationalKernel.restrictionIso line 243
  20. lemma OAI.SourceBurnside.Stability.RationalKernel.restrictionIso_apply line 248
  21. abbrev OAI.SourceBurnside.Stability.RationalKernel.cast line 257
  22. lemma OAI.SourceBurnside.Stability.RationalKernel.cast_refl line 261
  23. lemma OAI.SourceBurnside.Stability.RationalKernel.cast_succ line 266
  24. lemma OAI.SourceBurnside.Stability.RationalKernel.cast_mem line 273
  25. def OAI.SourceBurnside.Stability.RationalKernel.kernelCast line 280
  26. lemma OAI.SourceBurnside.Stability.RationalKernel.kernelCast_refl line 285
  27. lemma OAI.SourceBurnside.Stability.RationalKernel.kernelCast_succ line 290
  28. theorem OAI.SourceBurnside.Stability.RationalKernel.restriction_cast_surjective line 297
  29. lemma OAI.SourceBurnside.Stability.RationalDetection.character_nonzero_of_not_finite line 322
  30. lemma OAI.SourceBurnside.Stability.RationalDetection.finite_of_characters_vanish line 345
  31. lemma OAI.SourceBurnside.Stability.RationalDetection.character_finite_eq_one line 353