OAI/Geometry/HeilbronnTriangle/LatticeSplit.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.LatticeSplit.kernelProdEquiv line 10
  2. theorem OAI.Problem355.LatticeSplit.kernelProdEquiv_snd line 29
  3. theorem OAI.Problem355.LatticeSplit.kernelProdEquiv_fst_coe line 32
  4. theorem OAI.Problem355.LatticeSplit.kernelProdEquiv_symm_apply line 35
  5. theorem OAI.Problem355.LatticeSplit.existsUnique_kernel_component line 39
  6. def OAI.Problem355.LatticeSplit.extendKernelBasis line 48
  7. theorem OAI.Problem355.LatticeSplit.extendKernelBasis_inl line 52
  8. theorem OAI.Problem355.LatticeSplit.extendKernelBasis_inr line 57
  9. theorem OAI.Problem355.LatticeSplit.extendKernelBasis_repr_inr line 62
  10. def OAI.Problem355.LatticeSplit.restrictedKernelEquiv line 68
  11. theorem OAI.Problem355.LatticeSplit.restrictedKernelEquiv_apply_coe line 77
  12. def OAI.Problem355.LatticeSplit.divideIntFunctional line 84
  13. theorem OAI.Problem355.LatticeSplit.divideIntFunctional_apply line 94
  14. theorem OAI.Problem355.LatticeSplit.ker_divideIntFunctional line 98
  15. def OAI.Problem355.LatticeSplit.integerKernelProdEquiv line 111
  16. theorem OAI.Problem355.LatticeSplit.integerKernelProdEquiv_snd line 150
  17. theorem OAI.Problem355.LatticeSplit.integerKernelProdEquiv_fst_coe line 155
  18. theorem OAI.Problem355.LatticeSplit.integerKernelProdEquiv_symm_apply line 160
  19. def OAI.Problem355.LatticeSplit.extendIntegerKernelBasis line 165
  20. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis_inl line 171
  21. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis_inr line 177
  22. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis_repr_inr line 183
  23. theorem OAI.Problem355.LatticeSplit.exists_positive_image_generator line 190
  24. theorem OAI.Problem355.LatticeSplit.finrank_kernel_add_one line 209
  25. def OAI.Problem355.LatticeSplit.integerKernelBasisFin line 216
  26. theorem OAI.Problem355.LatticeSplit.finrank_kernel_add_one_of_ne_zero line 224
  27. theorem OAI.Problem355.LatticeSplit.exists_plane_kernel_basis line 230
  28. theorem OAI.Problem355.LatticeSplit.finrank_eq_of_scalar_containment line 235
  29. theorem OAI.Problem355.LatticeSplit.index_ne_zero_of_scalar_containment line 245
  30. theorem OAI.Problem355.LatticeSplit.exists_restricted_image_generator line 252
  31. theorem OAI.Problem355.LatticeSplit.exists_restricted_kernel_basis line 269