OAI/Combinatorics/SumProduct/Alignment/MalcevWeighted02.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MalcevWeightedCoordinates.exists_sorting_permutation line 21
  2. lemma OAI.MalcevWeightedCoordinates.exists_weight_cutoff line 43
  3. lemma OAI.RationalLattice.basisFlow_mem_subspace line 78
  4. lemma OAI.RationalLattice.peel_mem_subspace line 86
  5. lemma OAI.RationalLattice.expCoordinates_subspace line 101
  6. theorem OAI.RationalLattice.secondCoordinates_subspace line 120
  7. lemma OAI.MalcevWeightedCoordinates.exists_axis_out line 139
  8. def OAI.MalcevWeightedCoordinates.subspaceWeight line 146
  9. lemma OAI.MalcevWeightedCoordinates.weight_lt_iff_out line 152
  10. lemma OAI.MalcevWeightedCoordinates.axis_mem_subspace_iff line 172
  11. theorem OAI.MalcevWeightedCoordinates.subspaceWeight_level line 191
  12. theorem OAI.MalcevWeightedCoordinates.exists_adapted_secondKind_coordinates line 221