OAI/GroupTheory/UniversalGroup/FiniteEnvelopes.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.ModelAlgebra line 21
  2. def OAI.UniversalFInfinity.diagramElement line 24
  3. lemma OAI.UniversalFInfinity.diagramElement_one line 27
  4. lemma OAI.UniversalFInfinity.diagramElement_mul line 31
  5. lemma OAI.UniversalFInfinity.diagramElement_eq line 41
  6. lemma OAI.UniversalFInfinity.diagramElement_orthogonal_mul line 48
  7. lemma OAI.UniversalFInfinity.diagramElement_commute line 56
  8. lemma OAI.UniversalFInfinity.diagramElement_add line 63
  9. def OAI.UniversalFInfinity.diagramHom line 69
  10. lemma OAI.UniversalFInfinity.diagramHom_val line 79
  11. lemma OAI.UniversalFInfinity.diagramHom_commute line 82
  12. lemma OAI.UniversalFInfinity.diagramHom_add line 88
  13. lemma OAI.UniversalFInfinity.diagramHom_identity_val line 97
  14. lemma OAI.UniversalFInfinity.diagramHom_identity_injective line 102
  15. abbrev OAI.UniversalFInfinity.FiniteEnvelope.RelationIndex line 117
  16. def OAI.UniversalFInfinity.FiniteEnvelope.relationWord line 121
  17. abbrev OAI.UniversalFInfinity.FiniteEnvelope.relators line 132
  18. abbrev OAI.UniversalFInfinity.FiniteEnvelope.Envelope line 135
  19. instance OAI.UniversalFInfinity.FiniteEnvelope.finiteRelators line 138
  20. instance OAI.UniversalFInfinity.FiniteEnvelope.finitelyPresented line 142
  21. def OAI.UniversalFInfinity.FiniteEnvelope.copy line 149
  22. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_of line 154
  23. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_same line 157
  24. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_of_commute line 163
  25. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_of_sum line 169
  26. lemma OAI.UniversalFInfinity.FiniteEnvelope.commute_of_generators line 178
  27. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_commute line 192
  28. def OAI.UniversalFInfinity.FiniteEnvelope.commutingProduct line 196
  29. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_sum line 204
  30. lemma OAI.UniversalFInfinity.FiniteEnvelope.model_satisfies_relations line 220
  31. def OAI.UniversalFInfinity.FiniteEnvelope.modelMap line 241
  32. lemma OAI.UniversalFInfinity.FiniteEnvelope.modelMap_copy line 245
  33. lemma OAI.UniversalFInfinity.FiniteEnvelope.copy_injective_of_model line 250
  34. structure OAI.UniversalFInfinity.FiniteIdempotentSystem line 260
  35. instance OAI.UniversalFInfinity.FiniteIdempotentSystem.(instance at line 270) line 270
  36. def OAI.UniversalFInfinity.FiniteIdempotentSystem.identity line 272
  37. lemma OAI.UniversalFInfinity.FiniteIdempotentSystem.isIdempotent line 274
  38. abbrev OAI.UniversalFInfinity.TwoEnvelope.Index line 286
  39. def OAI.UniversalFInfinity.TwoEnvelope.common line 288
  40. def OAI.UniversalFInfinity.TwoEnvelope.triples line 291
  41. abbrev OAI.UniversalFInfinity.TwoEnvelope.ModelGroup line 301
  42. def OAI.UniversalFInfinity.TwoEnvelope.family line 303
  43. lemma OAI.UniversalFInfinity.TwoEnvelope.family_common line 314
  44. lemma OAI.UniversalFInfinity.TwoEnvelope.family_commute line 321
  45. lemma OAI.UniversalFInfinity.TwoEnvelope.family_sum line 335
  46. lemma OAI.UniversalFInfinity.TwoEnvelope.family_identity_injective line 359
  47. theorem OAI.UniversalFInfinity.TwoEnvelope.finite_envelope line 367