OAI/NumberTheory/PiExponent/Geometry/CurveComponentRigidity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveComponentRigidity.residueY_ne_zero line 13
2. def OAI.PiExponent.CurveComponentRigidity.NormalProductComparison line 19
3. def OAI.PiExponent.CurveComponentRigidity.PersistentNormalComparison line 31
4. theorem OAI.PiExponent.CurveComponentRigidity.coordinate_constant_of_persistent_comparison line 44
5. theorem OAI.PiExponent.CurveComponentRigidity.coordinate_eq_one_of_persistent_comparison line 78