OAI/Algebra/AffineCancellation/Modification.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ComplexCancellation.AffineModification.P line 12
  2. def OAI.ComplexCancellation.AffineModification.rel line 13
  3. abbrev OAI.ComplexCancellation.AffineModification.T line 14
  4. def OAI.ComplexCancellation.AffineModification.π line 15
  5. def OAI.ComplexCancellation.AffineModification.τ line 16
  6. def OAI.ComplexCancellation.AffineModification.V line 17
  7. lemma OAI.ComplexCancellation.AffineModification.equation line 20
  8. abbrev OAI.ComplexCancellation.AffineModification.F line 25
  9. abbrev OAI.ComplexCancellation.AffineModification.K line 26
  10. def OAI.ComplexCancellation.AffineModification.baseEmbedding line 27
  11. lemma OAI.ComplexCancellation.AffineModification.baseEmbedding_injective line 31
  12. lemma OAI.ComplexCancellation.AffineModification.baseEmbedding_X line 35
  13. lemma OAI.ComplexCancellation.AffineModification.X_nonzero line 39
  14. def OAI.ComplexCancellation.AffineModification.values line 41
  15. def OAI.ComplexCancellation.AffineModification.eval line 42
  16. lemma OAI.ComplexCancellation.AffineModification.eval_rel line 43
  17. def OAI.ComplexCancellation.AffineModification.embedding line 49
  18. lemma OAI.ComplexCancellation.AffineModification.embedding_π line 54
  19. def OAI.ComplexCancellation.AffineModification.baseMap line 57
  20. lemma OAI.ComplexCancellation.AffineModification.baseMap_X line 59
  21. lemma OAI.ComplexCancellation.AffineModification.embedding_baseMap line 61
  22. lemma OAI.ComplexCancellation.AffineModification.τ_regular line 66
  23. lemma OAI.ComplexCancellation.AffineModification.clears line 73
  24. lemma OAI.ComplexCancellation.AffineModification.embedding_injective line 86
  25. lemma OAI.ComplexCancellation.AffineModification.isDomain line 92