OAI/NumberTheory/PiExponent/LocalAlgebra/QuotientLocalizedLength.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W23.intrinsic_length_eq_of_ringEquiv line 10
2. theorem OAI.PiExponentSiegel.W23.quotient_module_length_eq_intrinsic line 22
3. theorem OAI.PiExponentSiegel.W23.parameterLocalizationMap_surjective line 29
4. theorem OAI.PiExponentSiegel.W23.quotient_localized_length_eq line 36
5. theorem OAI.PiExponentSiegel.W23.quotient_localized_length_eq_explicit line 51