OAI/NumberTheory/PiExponent/LocalAlgebra/RamifiedLocalLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.RamifiedLocalLength.residueField_map_surjective_of_mod_surjective line 9
2. theorem OAI.PiExponent.RamifiedLocalLength.closed_fibre_length_eq_finrank line 28
3. theorem OAI.PiExponent.RamifiedLocalLength.length_baseChange_eq_finrank_mul line 50
4. theorem OAI.PiExponent.RamifiedLocalLength.length_quotient_map_eq_finrank_mul line 57