OAI/NumberTheory/PiExponent/Geometry/SectionZeroStalk.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.SectionZeroStalk.stalkMap_ker_eq_map_affine_ker line 13
2. theorem OAI.PiExponent.SectionZeroStalk.zero_stalk_kernel line 44
3. def OAI.PiExponent.SectionZeroStalk.sectionGerm line 56
4. def OAI.PiExponent.SectionZeroStalk.zeroStalkQuotientEquiv line 61
5. theorem OAI.PiExponent.SectionZeroStalk.intrinsic_length_eq_of_ringEquiv line 72
6. theorem OAI.PiExponent.SectionZeroStalk.sectionGerm_ne_zero line 78
7. theorem OAI.PiExponent.SectionZeroStalk.zero_stalk_length_eq_order line 93