OAI/RingTheory/Tachikawa/Symmetry.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.k line 10

    Also declared: ComparatorChallenges/Tachikawa.lean:9 (same declaration text).

  2. def OAI.Tachikawa.SymmetricOver line 12

    Also declared: ComparatorChallenges/Tachikawa.lean:11 (same declaration text).

  3. def OAI.Tachikawa.Counterexample line 17

    Also declared: ComparatorChallenges/Tachikawa.lean:16 (same declaration text).

  4. def OAI.Tachikawa.DualBimodule line 41
  5. instance OAI.Tachikawa.DualBimodule.(instance at line 46) line 46
  6. instance OAI.Tachikawa.DualBimodule.(instance at line 47) line 47
  7. instance OAI.Tachikawa.DualBimodule.(instance at line 50) line 50
  8. instance OAI.Tachikawa.DualBimodule.(instance at line 51) line 51
  9. lemma OAI.Tachikawa.DualBimodule.ext line 53
  10. lemma OAI.Tachikawa.DualBimodule.add_apply line 55
  11. lemma OAI.Tachikawa.DualBimodule.zero_apply line 56
  12. lemma OAI.Tachikawa.DualBimodule.smul_apply line 57
  13. instance OAI.Tachikawa.DualBimodule.leftModule line 59
  14. lemma OAI.Tachikawa.DualBimodule.left_apply line 68
  15. instance OAI.Tachikawa.DualBimodule.rightModule line 70
  16. lemma OAI.Tachikawa.DualBimodule.right_apply line 85
  17. instance OAI.Tachikawa.DualBimodule.(instance at line 88) line 88
  18. instance OAI.Tachikawa.DualBimodule.(instance at line 91) line 91
  19. instance OAI.Tachikawa.DualBimodule.(instance at line 96) line 96
  20. instance OAI.Tachikawa.DualBimodule.(instance at line 101) line 101
  21. instance OAI.Tachikawa.DualBimodule.(instance at line 104) line 104
  22. instance OAI.Tachikawa.DualBimodule.(instance at line 107) line 107
  23. def OAI.Tachikawa.DualBimodule.coinduce line 118
  24. lemma OAI.Tachikawa.DualBimodule.coinduce_apply line 133
  25. instance OAI.Tachikawa.DualBimodule.injective line 137
  26. abbrev OAI.Tachikawa.TrivialExtension line 169
  27. instance OAI.Tachikawa.TrivialExtension.(instance at line 175) line 175
  28. def OAI.Tachikawa.TrivialExtension.trace line 178
  29. lemma OAI.Tachikawa.TrivialExtension.trace_apply line 183
  30. lemma OAI.Tachikawa.TrivialExtension.trace_mul line 185
  31. lemma OAI.Tachikawa.TrivialExtension.trace_comm line 190
  32. lemma OAI.Tachikawa.TrivialExtension.trace_nondegenerate line 193
  33. structure OAI.Tachikawa.SymmetrizingForm line 216
  34. def OAI.Tachikawa.SymmetrizingForm.toDual line 224
  35. lemma OAI.Tachikawa.SymmetrizingForm.toDual_apply line 226
  36. lemma OAI.Tachikawa.SymmetrizingForm.toDual_injective line 228
  37. def OAI.Tachikawa.SymmetrizingForm.dualEquiv line 237
  38. lemma OAI.Tachikawa.SymmetrizingForm.injective line 245
  39. def OAI.Tachikawa.TrivialExtension.symmetrizingForm line 262
  40. instance OAI.Tachikawa.TrivialExtension.(instance at line 267) line 267
  41. lemma OAI.Tachikawa.SymmetrizingForm.symmetricOver line 277
  42. lemma OAI.Tachikawa.TrivialExtension.symmetricOver line 289
  43. lemma OAI.Tachikawa.counterexampleOf line 297