OAI/Algebra/AffineCancellation/Quadric.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ComplexCancellation.Quadric.Poly line 10
  2. abbrev OAI.ComplexCancellation.Quadric.Base line 11
  3. abbrev OAI.ComplexCancellation.Quadric.K line 12
  4. def OAI.ComplexCancellation.Quadric.relation line 13
  5. abbrev OAI.ComplexCancellation.Quadric.R line 14
  6. def OAI.ComplexCancellation.Quadric.π line 15
  7. def OAI.ComplexCancellation.Quadric.x line 16
  8. def OAI.ComplexCancellation.Quadric.y line 17
  9. def OAI.ComplexCancellation.Quadric.z line 18
  10. def OAI.ComplexCancellation.Quadric.u line 19
  11. def OAI.ComplexCancellation.Quadric.s line 20
  12. def OAI.ComplexCancellation.Quadric.f line 21
  13. def OAI.ComplexCancellation.Quadric.g line 22
  14. def OAI.ComplexCancellation.Quadric.baseEmbedding line 24
  15. lemma OAI.ComplexCancellation.Quadric.baseEmbedding_injective line 25
  16. lemma OAI.ComplexCancellation.Quadric.x_field_nonzero line 26
  17. def OAI.ComplexCancellation.Quadric.values line 28
  18. def OAI.ComplexCancellation.Quadric.eval line 31
  19. lemma OAI.ComplexCancellation.Quadric.eval_relation line 32
  20. def OAI.ComplexCancellation.Quadric.embedding line 38
  21. lemma OAI.ComplexCancellation.Quadric.embedding_π line 42
  22. lemma OAI.ComplexCancellation.Quadric.equation line 43
  23. lemma OAI.ComplexCancellation.Quadric.x_regular line 47
  24. def OAI.ComplexCancellation.Quadric.baseMap line 53
  25. lemma OAI.ComplexCancellation.Quadric.baseMap_X_zero line 54
  26. lemma OAI.ComplexCancellation.Quadric.embedding_baseMap line 55
  27. lemma OAI.ComplexCancellation.Quadric.clears line 59
  28. lemma OAI.ComplexCancellation.Quadric.embedding_injective line 69
  29. instance OAI.ComplexCancellation.Quadric.(instance at line 74) line 74
  30. lemma OAI.ComplexCancellation.Quadric.baseMap_injective line 75
  31. lemma OAI.ComplexCancellation.Quadric.x_ne_zero line 79