OAI/GroupTheory/FiniteType/TwistedBrinSeparated.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwistedBrin.Prefix.separated line 12
2. lemma OAI.TwistedBrin.exists_displaced_brick line 35
3. lemma OAI.TwistedBrin.Localization.commute_of_disjoint_support line 71
4. lemma OAI.TwistedBrin.Localization.conjugate_outside line 95
5. lemma OAI.TwistedBrin.BrickSwap.stationary line 111
6. def OAI.TwistedBrin.SimplicityProducer.KillsBrick line 128
7. lemma OAI.TwistedBrin.SimplicityProducer.kills_disjoint line 130
8. lemma OAI.TwistedBrin.SimplicityProducer.kills_proper line 137
9. lemma OAI.TwistedBrin.SimplicityProducer.killed_displacer line 151
10. lemma OAI.TwistedBrin.SimplicityProducer.hom_eq_one_of_kills_proper line 177
11. lemma OAI.TwistedBrin.SimplicityProducer.hom_eq_one_of_nontrivial_kernel line 188
12. lemma OAI.TwistedBrin.localGroup_nontrivial line 197
13. theorem OAI.TwistedBrin.localGroup_simple line 214