OAI/Combinatorics/SumProduct/Alignment/MalcevWeighted01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MalcevSubspaceQuotient.prod_map_mul_of_central line 22
  2. lemma OAI.MalcevSubspaceQuotient.mk_coordinates_add_central line 41
  3. lemma OAI.MalcevSubspaceQuotient.mk_coordinates_central line 52
  4. lemma OAI.MalcevSubspaceQuotient.mask_central line 67
  5. lemma OAI.MalcevSubspaceQuotient.mask_compl_add_mask line 74
  6. theorem OAI.MalcevSubspaceQuotient.coord_mul_cut line 86
  7. lemma OAI.MalcevWeightedCoordinates.axis_mem_level line 148
  8. lemma OAI.MalcevWeightedCoordinates.axis_central_mod_next line 156
  9. theorem OAI.MalcevWeightedCoordinates.weighted_mul line 176
  10. def OAI.MalcevWeightedCoordinates.reorderHomeomorph line 198
  11. lemma OAI.MalcevWeightedCoordinates.lower_index line 212
  12. def OAI.MalcevWeightedCoordinates.lowerVector line 221
  13. lemma OAI.MalcevWeightedCoordinates.lowerVector_coordinates line 225
  14. lemma OAI.MalcevWeightedCoordinates.lower_correction_exists line 238
  15. def OAI.MalcevWeightedCoordinates.sortedCorrection line 253
  16. lemma OAI.MalcevWeightedCoordinates.sorted_mul line 261
  17. def OAI.MalcevWeightedCoordinates.sortedCoordinates line 276