OAI/Combinatorics/Chromatic/GradedAlgebra/FinitelySupportedUnitRows.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.UnitSelections.unitRowCount_sum line 13
  2. lemma OAI.ElementaryPositivity.UnitSelections.unitRowCount_zero_iff line 18
  3. abbrev OAI.ElementaryPositivity.UnitSelections.SupportedUnitRows line 30
  4. lemma OAI.ElementaryPositivity.UnitSelections.supportedRows_finite_nonempty line 33
  5. def OAI.ElementaryPositivity.UnitSelections.columnRow line 41
  6. def OAI.ElementaryPositivity.UnitSelections.columnRows line 45
  7. def OAI.ElementaryPositivity.UnitSelections.rowsColumn line 55
  8. def OAI.ElementaryPositivity.UnitSelections.allUnitRowsEquiv line 59
  9. lemma OAI.ElementaryPositivity.UnitSelections.allUnitRows_count line 78
  10. lemma OAI.ElementaryPositivity.UnitSelections.allUnitRows_energy line 84
  11. lemma OAI.ElementaryPositivity.UnitSelections.allUnitRows_dimension line 94
  12. def OAI.ElementaryPositivity.UnitSelections.rowFinsupp line 108
  13. lemma OAI.ElementaryPositivity.UnitSelections.rowFinsupp_equiv line 111
  14. def OAI.ElementaryPositivity.UnitSelections.rowsDimension line 116
  15. def OAI.ElementaryPositivity.UnitSelections.rowsEnergy line 119
  16. lemma OAI.ElementaryPositivity.UnitSelections.rowsDimension_equiv line 122
  17. lemma OAI.ElementaryPositivity.UnitSelections.rowsEnergy_equiv line 128