OAI/Algebra/OddKaplansky/QuadraticTower.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.QuadraticTower.polynomial line 15
  2. lemma OAI.OddKaplansky.QuadraticTower.polynomial_monic line 17
  3. lemma OAI.OddKaplansky.QuadraticTower.polynomial_degree line 20
  4. lemma OAI.OddKaplansky.QuadraticTower.polynomial_irreducible line 23
  5. def OAI.OddKaplansky.QuadraticTower.basis line 29
  6. lemma OAI.OddKaplansky.QuadraticTower.basis_dim line 32
  7. lemma OAI.OddKaplansky.QuadraticTower.basis_gen line 33
  8. instance OAI.OddKaplansky.QuadraticTower.finiteDimensional line 35
  9. lemma OAI.OddKaplansky.QuadraticTower.finrank line 38
  10. lemma OAI.OddKaplansky.QuadraticTower.root_sq line 41
  11. lemma OAI.OddKaplansky.QuadraticTower.norm_root line 48
  12. lemma OAI.OddKaplansky.QuadraticTower.root_not_isSquare line 56
  13. instance OAI.OddKaplansky.QuadraticTower.finite line 64
  14. lemma OAI.OddKaplansky.QuadraticTower.card line 67
  15. lemma OAI.OddKaplansky.QuadraticTower.exists_nonsquare_representative line 74
  16. def OAI.OddKaplansky.QuadraticTower.nonsquareIndex line 79
  17. def OAI.OddKaplansky.QuadraticTower.eta line 80
  18. lemma OAI.OddKaplansky.QuadraticTower.eta_not_isSquare line 82
  19. lemma OAI.OddKaplansky.QuadraticTower.eta_ne_zero line 84
  20. lemma OAI.OddKaplansky.QuadraticTower.nonsquareIndex_lt line 87
  21. lemma OAI.OddKaplansky.QuadraticTower.nonsquareIndex_min line 89
  22. abbrev OAI.OddKaplansky.QuadraticTower.FirstField line 95
  23. instance OAI.OddKaplansky.QuadraticTower.first_irreducible line 96
  24. instance OAI.OddKaplansky.QuadraticTower.first_fintype line 98
  25. def OAI.OddKaplansky.QuadraticTower.xi line 100
  26. abbrev OAI.OddKaplansky.QuadraticTower.CoeffField line 102
  27. theorem OAI.OddKaplansky.QuadraticTower.second_irreducible line 103
  28. def OAI.OddKaplansky.QuadraticTower.coeffField line 108
  29. instance OAI.OddKaplansky.QuadraticTower.tower_fintype line 111
  30. lemma OAI.OddKaplansky.QuadraticTower.first_card line 113
  31. lemma OAI.OddKaplansky.QuadraticTower.tower_card line 115