OAI/Topology/ArtinGroups/Harmonic/CosetSignUpperTie.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceCosetSign_eq_at_upper_tie line 14
2. theorem OAI.HarmonicArtin.sourceUpper_inactive_later line 24
3. theorem OAI.HarmonicArtin.sourceUpper_earlier_has_active line 59
4. theorem OAI.HarmonicArtin.sourceUpper_active_earlier line 66