OAI/Topology/ArtinGroups/Harmonic/ProbeCoreInclusion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.probeCoreInclusion line 20
2. lemma OAI.HarmonicArtin.probeCoreInclusion_injective line 24
3. lemma OAI.HarmonicArtin.probeCore_matrix line 27
4. lemma OAI.HarmonicArtin.probeCore_simply_laced line 42
5. lemma OAI.HarmonicArtin.probePositiveWord_core_expanded line 53
6. lemma OAI.HarmonicArtin.probeCore_word_support line 59
7. lemma OAI.HarmonicArtin.probePositiveWord_testUpper_reflect line 66
8. lemma OAI.HarmonicArtin.probeCore_cons_reduced line 73
9. theorem OAI.HarmonicArtin.probe_reduced_ascent_top_exact line 95