OAI/NumberTheory/PrimePackets/AdelicPatch.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.Adelic.finiteMatrixAt line 11
  2. lemma OAI.PrimeDegreePackets.Adelic.finiteMatrixAt_inv line 15
  3. def OAI.PrimeDegreePackets.Adelic.localIntegralRows line 20
  4. def OAI.PrimeDegreePackets.Adelic.localMatrixLattice line 27
  5. def OAI.PrimeDegreePackets.Adelic.basisFullLattice line 35
  6. lemma OAI.PrimeDegreePackets.Adelic.basisFullLattice_basis line 41
  7. lemma OAI.PrimeDegreePackets.Adelic.completed_basisFullLattice line 45
  8. lemma OAI.PrimeDegreePackets.Adelic.mem_localMatrixLattice_iff line 52
  9. lemma OAI.PrimeDegreePackets.Adelic.finiteGlobalMatrixLattice_local_iff line 59
  10. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_open line 82
  11. lemma OAI.PrimeDegreePackets.Adelic.open_submodule_absorbs_fullLattice line 99
  12. theorem OAI.PrimeDegreePackets.Adelic.patch_open_local_modules line 128
  13. lemma OAI.PrimeDegreePackets.Adelic.finite_family_integral_denominator line 154
  14. lemma OAI.PrimeDegreePackets.Adelic.integral_vecMul line 186
  15. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_eq_of_integral line 195
  16. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_eventually_eq line 210
  17. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_mul_denominator line 222
  18. lemma OAI.PrimeDegreePackets.Adelic.local_integral_scalar_smul_eq line 237
  19. lemma OAI.PrimeDegreePackets.Adelic.completed_scale_eventually_eq line 251
  20. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_le_scaled_basis line 263
  21. theorem OAI.PrimeDegreePackets.Adelic.finite_matrix_lattice_full_and_completed line 280