OAI/NumberTheory/PiExponent/Geometry/ReducedComponentStalk.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveCycle.reducedComponentι_range line 10
  2. theorem OAI.PiExponent.CurveCycle.reducedComponentι_mem line 16
  3. theorem OAI.PiExponent.CurveCycle.reducedComponentι_genericPoint line 21
  4. theorem OAI.PiExponent.CurveCycle.fromSpecStalk_bot_eq_genericPoint line 31
  5. def OAI.PiExponent.CurveCycle.reducedComponentStalkPrime line 41
  6. theorem OAI.PiExponent.CurveCycle.reducedComponentι_stalkMap_ker line 46
  7. def OAI.PiExponent.CurveCycle.reducedComponentStalkQuotientEquiv line 70
  8. theorem OAI.PiExponent.CurveCycle.reducedComponentStalkQuotientEquiv_mk line 80
  9. theorem OAI.PiExponent.CurveCycle.reducedComponentι_stalkMap_ne_zero line 89