OAI/NumberTheory/PiExponent/LocalAlgebra/LocalIntersectionLength.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W28.LocalIntersection.finite_length_kernel_eq_cokernel line 11
2. def OAI.PiExponentJets.W28.LocalIntersection.quotientMul line 32
3. theorem OAI.PiExponentJets.W28.LocalIntersection.quotientMul_apply line 35
4. theorem OAI.PiExponentJets.W28.LocalIntersection.quotientMul_mk line 38
5. theorem OAI.PiExponentJets.W28.LocalIntersection.quotientMul_kernel line 45
6. def OAI.PiExponentJets.W28.LocalIntersection.colonQuotientEquivKernel line 64
7. theorem OAI.PiExponentJets.W28.LocalIntersection.quotientMul_range line 70
8. def OAI.PiExponentJets.W28.LocalIntersection.cokernelEquivCut line 82
9. theorem OAI.PiExponentJets.W28.LocalIntersection.kernel_length_eq_colon line 88
10. theorem OAI.PiExponentJets.W28.LocalIntersection.cokernel_length_eq_cut line 93
11. theorem OAI.PiExponentJets.W28.LocalIntersection.finite_length_cut_eq_colon line 98
12. theorem OAI.PiExponentJets.W28.LocalIntersection.regular_colon_length_zero line 105