OAI/NumberTheory/PiExponent/LocalAlgebra/RamifiedPowerLength.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.RamifiedLocalLength.coverOriginIdeal line 16
2. instance OAI.PiExponent.RamifiedLocalLength.coverOriginIdeal_isMaximal line 20
3. theorem OAI.PiExponent.RamifiedLocalLength.coverOriginIdeal_liesOver line 25
4. theorem OAI.PiExponent.RamifiedLocalLength.coverOriginIdeal_unique line 35
5. def OAI.PiExponent.RamifiedLocalLength.coverOriginLocalEquiv line 65
6. def OAI.PiExponent.RamifiedLocalLength.translatedPowerLocalBasis line 71
7. theorem OAI.PiExponent.RamifiedLocalLength.translatedPowerLocal_finrank line 100
8. theorem OAI.PiExponent.RamifiedLocalLength.translatedPowerLocal_quotient_length line 109