OAI/GroupTheory/FiniteLattice/LabelledCollection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Collection of subgroup factors by labels. The error subgroup normalizes each factor; it need not be normal in the generated group.

  1. def OAI.FiniteLattice.LabelledCollection.generated line 15
  2. lemma OAI.FiniteLattice.LabelledCollection.generator_mem line 18
  3. lemma OAI.FiniteLattice.LabelledCollection.conjugate_generated line 22
  4. lemma OAI.FiniteLattice.LabelledCollection.move_labelled_word line 39
  5. theorem OAI.FiniteLattice.LabelledCollection.collection_flattened line 85
  6. lemma OAI.FiniteLattice.LabelledCollection.generated_labels line 126
  7. theorem OAI.FiniteLattice.LabelledCollection.collection line 145