OAI/Combinatorics/SumProduct/Alignment/RationalLattice06.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.realPower_int line 25
  2. lemma OAI.RationalLattice.basisElement_rational line 32
  3. lemma OAI.RationalLattice.basisFlow_rational line 39
  4. lemma OAI.RationalLattice.basisElement_mem line 46
  5. lemma OAI.RationalLattice.basisFlow_int_mem line 54
  6. lemma OAI.RationalLattice.peel_mem_lattice line 59
  7. theorem OAI.RationalLattice.expCoordinates_lattice line 72
  8. theorem OAI.RationalLattice.character_expCoordinates line 90
  9. theorem OAI.RationalLattice.integer_character_expCoordinates line 104
  10. theorem OAI.CharacterKernelLattice.compact_kernel_representatives line 132
  11. theorem OAI.CharacterKernelLattice.compact_kernel_representatives_inter line 185
  12. lemma OAI.MalcevCharacters.character_ext_coordinates line 209
  13. theorem OAI.MalcevCharacters.bounded_integral_characters_finite line 221
  14. theorem OAI.MalcevCharacters.kernel_inter_connected line 251
  15. theorem OAI.MalcevCharacters.nontrivial_kernel_geometry line 273