OAI/NumberTheory/PiExponent/LocalAlgebra/ConeEquationLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.conePrimeLocalizationEquiv_algebraMap line 14
2. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.conePrimeLocalizationEquiv_map_ideal line 37
3. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affine_ideal_map_to_laurent_local line 49
4. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.homogenized_cone_local_length_eq line 63