OAI/Topology/ArtinGroups/Harmonic/Block.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HarmonicArtin.SourceBlock line 13
  2. def OAI.HarmonicArtin.sourceBlock line 15
  3. def OAI.HarmonicArtin.sourceZeroBlock line 18
  4. def OAI.HarmonicArtin.SourceBlockOccurs line 20
  5. lemma OAI.HarmonicArtin.sourceBlock_of_vector_zero line 23
  6. lemma OAI.HarmonicArtin.sourceCosetSum_pos_of_ne_zero line 33
  7. lemma OAI.HarmonicArtin.sourceZeroBlock_le line 44
  8. lemma OAI.HarmonicArtin.sourceBlock_bounded_finite line 52
  9. lemma OAI.HarmonicArtin.sourceBlock_predecessors_finite line 67
  10. def OAI.HarmonicArtin.sourceBlockRank line 73
  11. lemma OAI.HarmonicArtin.sourceBlockRank_strictMono line 76
  12. lemma OAI.HarmonicArtin.sourceBlockRank_lt_iff line 83
  13. lemma OAI.HarmonicArtin.sourceBlockRank_eq_iff line 94
  14. lemma OAI.HarmonicArtin.sourceBlockRank_zero line 105
  15. lemma OAI.HarmonicArtin.sourceBlockRank_support_finite line 113
  16. def OAI.HarmonicArtin.sourceHeight line 124
  17. lemma OAI.HarmonicArtin.sourceHeight_lt_iff line 128
  18. theorem OAI.HarmonicArtin.sourceHeight_wellFounded line 140