OAI/Combinatorics/SumProduct/Alignment/IntegerHyperplane02.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCoverCharacter.uniform_power_mem line 26
  2. theorem OAI.FiniteCoverCharacter.integral_character_multiplier line 37
  3. theorem OAI.FactorCoefficientTransfer.finite_cover_factor_transfer line 81
  4. def OAI.IntegerHyperplane.splitLift line 174
  5. def OAI.IntegerHyperplane.splitCoordinates line 177
  6. lemma OAI.IntegerHyperplane.splitLift_succAbove line 180
  7. lemma OAI.IntegerHyperplane.splitLift_pivot line 185
  8. lemma OAI.IntegerHyperplane.form_splitLift line 191
  9. lemma OAI.IntegerHyperplane.splitCoordinates_splitLift line 197
  10. lemma OAI.IntegerHyperplane.splitLift_splitCoordinates line 205
  11. lemma OAI.IntegerHyperplane.splitLift_continuous line 223
  12. lemma OAI.IntegerHyperplane.splitCoordinates_continuous line 235
  13. def OAI.IntegerHyperplane.splitHomeomorph line 245
  14. lemma OAI.IntegerHyperplane.splitLift_polynomial line 254
  15. lemma OAI.IntegerHyperplane.splitLift_lower_dep line 266