OAI/GroupTheory/SimpleOvergroups/SemanticProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.Mon line 19
  2. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.pairEval line 21
  3. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.evaluation line 32
  4. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.pairEval_surjective line 36
  5. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.evaluation_surjective line 44
  6. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.normal line 47
  7. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.value line 50
  8. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.normal_eq_iff line 54
  9. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.normal_eq_zero line 60
  10. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.value_eq_iff line 65
  11. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.value_eq_none line 85
  12. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticProduct.full line 93