OAI/NumberTheory/PiExponent/Jets/FilteredLength.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.W24.filtrationRestriction line 12
2. def OAI.PiExponentJets.W24.filtrationLayerMap line 17
3. theorem OAI.PiExponentJets.W24.correction_of_layer_surjective line 26
4. theorem OAI.PiExponentJets.W24.surjective_of_finite_corrections line 40
5. theorem OAI.PiExponentJets.W24.surjective_of_finite_layers line 60
6. theorem OAI.PiExponentJets.W24.length_le_of_finite_layers line 71
7. theorem OAI.PiExponentJets.W24.scalar_lift_difference line 84