OAI/Algebra/OddKaplansky/Amalgam.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.MultipleHNN.con line 17
  2. def OAI.OddKaplansky.MultipleHNN.Extension line 21
  3. instance OAI.OddKaplansky.MultipleHNN.(instance at line 23) line 23
  4. def OAI.OddKaplansky.MultipleHNN.of line 25
  5. def OAI.OddKaplansky.MultipleHNN.letter line 27
  6. lemma OAI.OddKaplansky.MultipleHNN.letter_mul_of line 29
  7. def OAI.OddKaplansky.MultipleHNN.lift line 33
  8. lemma OAI.OddKaplansky.MultipleHNN.lift_of line 39
  9. lemma OAI.OddKaplansky.MultipleHNN.lift_letter line 45
  10. theorem OAI.OddKaplansky.MultipleHNN.finite_partial_realization line 51
  11. theorem OAI.OddKaplansky.MultipleHNN.of_injective line 80
  12. theorem OAI.OddKaplansky.MultipleHNN.induction_on line 88
  13. theorem OAI.OddKaplansky.MultipleHNN.of_central line 108
  14. instance OAI.OddKaplansky.MultipleHNN.(instance at line 121) line 121
  15. abbrev OAI.OddKaplansky.StarAmalgam.Free line 149
  16. def OAI.OddKaplansky.StarAmalgam.con line 151
  17. def OAI.OddKaplansky.StarAmalgam.Amalgam line 154
  18. instance OAI.OddKaplansky.StarAmalgam.(instance at line 155) line 155
  19. def OAI.OddKaplansky.StarAmalgam.ofBase line 157
  20. def OAI.OddKaplansky.StarAmalgam.ofFactor line 159
  21. lemma OAI.OddKaplansky.StarAmalgam.identify line 162
  22. def OAI.OddKaplansky.StarAmalgam.lift line 165
  23. lemma OAI.OddKaplansky.StarAmalgam.lift_base line 171
  24. lemma OAI.OddKaplansky.StarAmalgam.lift_factor line 177
  25. theorem OAI.OddKaplansky.StarAmalgam.faithful_realization line 183
  26. theorem OAI.OddKaplansky.StarAmalgam.ofBase_injective line 225
  27. theorem OAI.OddKaplansky.StarAmalgam.ofFactor_injective line 232