OAI/Combinatorics/SumProduct/Alignment/MalcevCharacters01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalLattice.rationalHom_origin_grid line 30
  2. theorem OAI.RationalLattice.exists_integer_sublattice line 69
  3. def OAI.FiniteCoverCharacters.denominator line 114
  4. lemma OAI.FiniteCoverCharacters.denominator_pos line 117
  5. lemma OAI.FiniteCoverCharacters.pow_denominator_mem line 121
  6. lemma OAI.FiniteCoverCharacters.integral_after_scaling line 128
  7. lemma OAI.MalcevCharacters.quotient_coord_add line 156
  8. def OAI.MalcevCharacters.quotientParameterHom line 175
  9. lemma OAI.MalcevCharacters.quotientParameterHom_surjective line 187
  10. def OAI.MalcevCharacters.linearParameterHom line 193
  11. lemma OAI.MalcevCharacters.parameter_kernel_le line 203
  12. def OAI.MalcevCharacters.abelianCoordinateCharacter line 210
  13. lemma OAI.MalcevCharacters.abelianCoordinateCharacter_apply line 215
  14. lemma OAI.MalcevCharacters.abelianCoordinateCharacter_continuous line 232
  15. lemma OAI.MalcevCharacters.coordinate_form_mul line 241
  16. lemma OAI.RationalTailCoordinates.lift_single line 261
  17. lemma OAI.RationalTailCoordinates.axis_val line 283
  18. lemma OAI.RationalTailCoordinates.tail_secondKind line 290