OAI/Combinatorics/EuclideanRamsey/AdicLifting.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanRamsey.nil_exp_quadratic line 30
  2. lemma OAI.EuclideanRamsey.nil_exp_eq_one_iff line 46
  3. lemma OAI.EuclideanRamsey.nil_exp_sub_one_sub_mem line 57
  4. lemma OAI.EuclideanRamsey.nil_exp_sub_one_mem line 75
  5. lemma OAI.EuclideanRamsey.nilpotent_of_mem_nil_ideal line 83
  6. lemma OAI.EuclideanRamsey.nil_ideal_exp_surjective line 89
  7. lemma OAI.EuclideanRamsey.nil_exp_injective line 131
  8. def OAI.EuclideanRamsey.characterLog line 144
  9. lemma OAI.EuclideanRamsey.characterLog_mem line 147
  10. lemma OAI.EuclideanRamsey.characterLog_exp line 150
  11. def OAI.EuclideanRamsey.characterLogHom line 155
  12. lemma OAI.EuclideanRamsey.characterLog_map_zero line 169
  13. def OAI.EuclideanRamsey.rationalExtension line 181
  14. lemma OAI.EuclideanRamsey.rationalExtension_lattice line 186
  15. lemma OAI.EuclideanRamsey.rationalExtension_mem line 198
  16. lemma OAI.EuclideanRamsey.adic_kernel_lifting line 213
  17. lemma OAI.EuclideanRamsey.adic_intersection_lifting line 240
  18. lemma OAI.EuclideanRamsey.rationalExtension_single line 272
  19. lemma OAI.EuclideanRamsey.tensor_quotient_quadratic line 278
  20. def OAI.EuclideanRamsey.cosetMap line 289
  21. def OAI.EuclideanRamsey.cosetIdeal line 293
  22. lemma OAI.EuclideanRamsey.mem_cosetIdeal_iff line 296
  23. lemma OAI.EuclideanRamsey.monomial_sub_one_mem_cosetIdeal line 302
  24. lemma OAI.EuclideanRamsey.quotient_nil_augmentation line 311
  25. lemma OAI.EuclideanRamsey.finite_order_logs line 316
  26. lemma OAI.EuclideanRamsey.log_quadratic_mod_coset line 337
  27. lemma OAI.EuclideanRamsey.finite_order_log_lifts line 376
  28. theorem OAI.EuclideanRamsey.finite_lattice_identity line 422