OAI/NumberTheory/PiExponent/LocalAlgebra/RegularSequenceExt.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSiegelAux.W31.regularSequenceAugmentation line 15
2. theorem OAI.PiExponentSiegelAux.W31.regularSequenceAugmentation_spec line 20
3. def OAI.PiExponentSiegelAux.W31.regularSequenceResolution line 29
4. theorem OAI.PiExponentSiegelAux.W31.regularSequenceResolution_complex line 43
5. def OAI.PiExponentSiegelAux.W31.regularSequenceQuotientExtAddEquiv line 47
6. theorem OAI.PiExponentSiegelAux.W31.regularSequenceQuotientExt_iff_boundaries line 55
7. theorem OAI.PiExponentSiegelAux.W31.regularSequenceQuotientExt_above_length line 64
8. theorem OAI.PiExponentSiegelAux.W31.regularSequenceQuotientExt_of_dual_exact line 72
9. def OAI.PiExponentSiegelAux.W31.residueFieldExtAddEquiv line 89