OAI/NumberTheory/PiExponent/LocalAlgebra/ConeRegularSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.ofList_map_mul_units line 19
2. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.isRegular_map_mul_units line 32
3. def OAI.PiExponentSiegel.W17.ConeLocalLength.coneLocalCoordinate line 58
4. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneLocalCoordinate_isUnit line 61
5. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.homogenized_local_eq_affine_mul_coordinate line 66
6. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affineLocalToConeLocal_faithfullyFlat line 97
7. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.homogenized_list_regular_at_cone line 109