OAI/Algebra/AffineCancellation/Determinant.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ComplexCancellation.Determinant.regular_quotient_of_prime line 10
  2. abbrev OAI.ComplexCancellation.Determinant.Poly line 26
  3. abbrev OAI.ComplexCancellation.Determinant.Base line 27
  4. abbrev OAI.ComplexCancellation.Determinant.Coeff line 28
  5. abbrev OAI.ComplexCancellation.Determinant.K₀ line 29
  6. abbrev OAI.ComplexCancellation.Determinant.K line 30
  7. def OAI.ComplexCancellation.Determinant.relation line 32
  8. abbrev OAI.ComplexCancellation.Determinant.T line 33
  9. def OAI.ComplexCancellation.Determinant.π line 34
  10. def OAI.ComplexCancellation.Determinant.a line 35
  11. def OAI.ComplexCancellation.Determinant.d line 36
  12. def OAI.ComplexCancellation.Determinant.b line 37
  13. def OAI.ComplexCancellation.Determinant.c line 38
  14. def OAI.ComplexCancellation.Determinant.u line 39
  15. def OAI.ComplexCancellation.Determinant.v line 40
  16. def OAI.ComplexCancellation.Determinant.baseEmbedding line 42
  17. lemma OAI.ComplexCancellation.Determinant.baseEmbedding_injective line 47
  18. lemma OAI.ComplexCancellation.Determinant.baseEmbedding_X_zero line 52
  19. lemma OAI.ComplexCancellation.Determinant.baseEmbedding_X_succ line 57
  20. def OAI.ComplexCancellation.Determinant.targetValues line 63
  21. def OAI.ComplexCancellation.Determinant.eval line 67
  22. lemma OAI.ComplexCancellation.Determinant.a_field_nonzero line 69
  23. lemma OAI.ComplexCancellation.Determinant.eval_relation line 74
  24. def OAI.ComplexCancellation.Determinant.embedding line 81
  25. lemma OAI.ComplexCancellation.Determinant.embedding_π line 86
  26. lemma OAI.ComplexCancellation.Determinant.determinant line 89
  27. lemma OAI.ComplexCancellation.Determinant.a_regular line 93
  28. def OAI.ComplexCancellation.Determinant.baseValues line 99
  29. def OAI.ComplexCancellation.Determinant.baseMap line 100
  30. lemma OAI.ComplexCancellation.Determinant.embedding_baseMap line 102
  31. lemma OAI.ComplexCancellation.Determinant.baseMap_injective line 109
  32. lemma OAI.ComplexCancellation.Determinant.clears_generator line 114
  33. lemma OAI.ComplexCancellation.Determinant.clears line 126
  34. lemma OAI.ComplexCancellation.Determinant.embedding_injective line 146
  35. instance OAI.ComplexCancellation.Determinant.(instance at line 156) line 156