OAI/NumberTheory/PiExponent/Approximation/SerrePowerDescent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.GeometrySupport.SerrePowerDescent.ext_zero_of_iso line 14
2. def OAI.PiExponent.GeometrySupport.SerrePowerDescent.moduleTwistLineIso line 22
3. theorem OAI.PiExponent.GeometrySupport.SerrePowerDescent.eventual_twist_ext_zero_of_lineIso line 27
4. def OAI.PiExponent.GeometrySupport.SerrePowerDescent.residueTwistIso line 37
5. theorem OAI.PiExponent.GeometrySupport.SerrePowerDescent.eventual_twist_ext_zero_of_power line 45