OAI/Topology/ArtinGroups/Harmonic/ProbePositiveWord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceProbePacket_as_packet line 21
2. def OAI.HarmonicArtin.probePositiveWord line 34
3. def OAI.HarmonicArtin.probeBottomWord line 38
4. lemma OAI.HarmonicArtin.probePositiveWord_cons line 42
5. lemma OAI.HarmonicArtin.probePositiveWord_expanded line 47
6. lemma OAI.HarmonicArtin.probePositiveWord_lowerBound line 57
7. lemma OAI.HarmonicArtin.probePositiveWord_reduced_eq line 63
8. lemma OAI.HarmonicArtin.probeBottomWord_cons_socle_zero line 81
9. theorem OAI.HarmonicArtin.probeBottomWord_socle_ascent line 91
10. theorem OAI.HarmonicArtin.probe_family_socle_finite_termination line 114