OAI/Topology/ArtinGroups/Harmonic/PositiveSupportComponent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.PositiveSupportComponent line 12
  2. def OAI.HarmonicArtin.harmonicPositiveSign line 18
  3. def OAI.HarmonicArtin.levelIncident line 24
  4. def OAI.HarmonicArtin.incidenceIndices line 28
  5. def OAI.HarmonicArtin.incidenceLevel line 32
  6. def OAI.HarmonicArtin.harmonicActive line 36
  7. theorem OAI.HarmonicArtin.levelIncident_support line 42
  8. theorem OAI.HarmonicArtin.levelIncident_mem line 49
  9. theorem OAI.HarmonicArtin.levelIncident_le line 54
  10. theorem OAI.HarmonicArtin.incidenceLevel_incident line 59
  11. theorem OAI.HarmonicArtin.no_incidence_row_zero line 69
  12. theorem OAI.HarmonicArtin.harmonic_active_component_posDef line 86
  13. theorem OAI.HarmonicArtin.matrix_posDef_of_fibers line 173
  14. theorem OAI.HarmonicArtin.matrix_posDef_of_connected line 224
  15. theorem OAI.HarmonicArtin.harmonic_active_posDef line 249