OAI/NumberTheory/PiExponent/LocalAlgebra/LocalIntersectionTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W28.LocalIntersection.map_scalar_kernel line 11
2. theorem OAI.PiExponentJets.W28.LocalIntersection.map_scalar_range line 26
3. def OAI.PiExponentJets.W28.LocalIntersection.scalarKernelEquiv line 40
4. def OAI.PiExponentJets.W28.LocalIntersection.scalarCokernelEquiv line 45
5. theorem OAI.PiExponentJets.W28.LocalIntersection.scalar_kernel_length_eq line 50
6. theorem OAI.PiExponentJets.W28.LocalIntersection.scalar_cokernel_length_eq line 55
7. theorem OAI.PiExponentJets.W28.LocalIntersection.cyclic_factor_kernel_length line 60
8. theorem OAI.PiExponentJets.W28.LocalIntersection.cyclic_factor_cokernel_length line 69