OAI/GroupTheory/SimpleOvergroups/EnlargementCore.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceEnlargement.value line 10
  2. lemma OAI.SourceEnlargement.value_one line 13
  3. lemma OAI.SourceEnlargement.value_mul line 17
  4. def OAI.SourceEnlargement.unitMap line 26
  5. lemma OAI.SourceEnlargement.unitMap_val line 35
  6. lemma OAI.SourceEnlargement.value_identity line 38
  7. lemma OAI.SourceEnlargement.unitMap_identity_injective line 41
  8. lemma OAI.SourceEnlargement.complement_product line 48
  9. lemma OAI.SourceEnlargement.value_mul_orthogonal line 54
  10. lemma OAI.SourceEnlargement.unitMap_commute line 65
  11. lemma OAI.SourceEnlargement.unitMap_add line 73
  12. def OAI.SourceEnlargement.indexAction line 81
  13. lemma OAI.SourceEnlargement.indexAction_single line 97
  14. lemma OAI.SourceEnlargement.scalar_index_commute line 101
  15. def OAI.SourceEnlargement.ringAction line 108
  16. lemma OAI.SourceEnlargement.ringAction_single line 112
  17. instance OAI.SourceEnlargement.unitsAction line 119
  18. lemma OAI.SourceEnlargement.unitMap_basis line 126
  19. lemma OAI.SourceEnlargement.unitMap_fixes line 135
  20. def OAI.SourceEnlargement.group line 140
  21. def OAI.SourceEnlargement.map line 145
  22. lemma OAI.SourceEnlargement.map_val line 149
  23. lemma OAI.SourceEnlargement.map_identity_injective line 152
  24. lemma OAI.SourceEnlargement.map_identity_basis line 158
  25. lemma OAI.SourceEnlargement.basis_injective line 163
  26. lemma OAI.SourceEnlargement.map_fixes line 167
  27. lemma OAI.SourceEnlargement.map_commute line 171
  28. lemma OAI.SourceEnlargement.map_add line 177