OAI/NumberTheory/SiegelZeros/LocalAlgebra/ResidueDirectionSelection.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localization_derivation_ext_module line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.kernel_finrank_three_of_finrank_four line 38
  3. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.basisOfIndependentTriple line 46
  4. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.basisOfIndependentTriple_apply line 52
  5. abbrev OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.Local line 60
  6. abbrev OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.Residue line 65
  7. abbrev OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.Maximal line 73
  8. abbrev OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.ResidueDerivation line 88
  9. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalDerivation line 99
  10. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residueCoordinate line 102
  11. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residueCoordinate_ne_zero line 105
  12. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalDerivation_coordinate line 110
  13. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residue_derivation_ext line 125
  14. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientMap line 143
  15. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientMap_original line 148
  16. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientMap_injective line 160
  17. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residueInvariant line 167
  18. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientMap_residueInvariant line 172
  19. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residueCoefficientEquiv line 179
  20. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientForm line 186
  21. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localLogForm line 191
  22. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localLogForm_eq line 199
  23. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localLogForm_original line 210
  24. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localLogForm_ne_zero line 216
  25. instance OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.residueDerivation_finite line 225
  26. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.localLogForm_kernel_finrank line 227
  27. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalKernelVectors line 239
  28. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalKernelVectors_linearIndependent line 246
  29. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalResidueBasis line 259
  30. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.originalResidueBasis_apply line 264
  31. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.original_basis_selected_normals line 284
  32. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.coefficientForm_omega line 304
  33. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.omegaCoefficients_ne_zero line 310
  34. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticKernelVectors line 315
  35. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticKernelVectors_linearIndependent line 322
  36. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticCoordinateBasis line 328
  37. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticCoordinateBasis_apply line 334
  38. def OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticResidueBasis line 339
  39. theorem OAI.SiegelZeros.WeightedTorusJets.ResidueDirectionBasis.biquadraticResidueBasis_apply line 345