OAI/Topology/ArtinGroups/Harmonic/InitialProbe.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.sourceInitialProbe line 20
2. lemma OAI.HarmonicArtin.sourceInitialProbe_cap line 23
3. lemma OAI.HarmonicArtin.probePositiveWord_initial_top line 27
4. lemma OAI.HarmonicArtin.probePositiveWord_factor line 45
5. theorem OAI.HarmonicArtin.positive_equal_probe_fraction line 53