OAI/NumberTheory/PiExponent/Geometry/CurveInequalityIntrinsic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveInequality.nonconstant_coordinates line 17
2. theorem OAI.PiExponent.CurveInequality.weighted_curve_inequality line 26
3. theorem OAI.PiExponent.CurveInequality.admissible_weighted_curve_inequality line 71