OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal03.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RealCharacters.scaledFamily line 24
  2. lemma OAI.RealCharacters.mem_scaledFamily line 27
  3. lemma OAI.RealCharacters.scaledFamily_continuous line 32
  4. lemma OAI.RealCharacters.scaledFamily_integral line 39
  5. def OAI.MalcevHorizontal.boundedCharacters line 53
  6. lemma OAI.MalcevHorizontal.mem_boundedCharacters line 57
  7. lemma OAI.MalcevHorizontal.boundedCharacters_continuous line 62
  8. lemma OAI.MalcevHorizontal.boundedCharacters_integral line 69
  9. theorem OAI.MalcevHorizontal.uniform_character_or_proper_factorization line 102
  10. lemma OAI.LeibmanSquare.lattice_linear_normalization line 199
  11. lemma OAI.LeibmanSquare.polynomial_conjugate line 216
  12. lemma OAI.LeibmanSquare.constant_normalization line 227
  13. theorem OAI.SquareInduction.uniform_dense_linear_square_descent line 258