OAI/NumberTheory/PiExponent/Approximation/ConstantPullbackDegree.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ConstantPullbackDegree.pullbackFrame_of_range_subset line 13
2. def OAI.PiExponent.ConstantPullbackDegree.constantPullbackIso line 27
3. theorem OAI.PiExponent.ConstantPullbackDegree.euler_difference_eq_zero line 37
4. theorem OAI.PiExponent.ConstantPullbackDegree.euler_difference_eq_zero_of_constant line 45
5. theorem OAI.PiExponent.ConstantPullbackDegree.curveDegree_eq_zero_of_contracted line 52