OAI/Combinatorics/Progressions/Estimates/SquareSymbolRelative.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquareSymbol_lie_eq_zero line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolKernel_lie_eq_zero line 39
  3. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolKernel_bch line 52
  4. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolMap_symbol line 71
  5. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolMap_diagonal line 75
  6. def OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolHom line 80
  7. def OAI.Erdos3.NilpotentLieFiltration.squareDiagonalSymbolHom line 83
  8. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndSymbolHom_diagonal line 86
  9. def OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart line 91
  10. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart_projection line 95
  11. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart_coord_kernel line 99
  12. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart_factorization line 103
  13. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart_mul line 107
  14. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelativeGroupPart_mul_coord line 116
  15. theorem OAI.Erdos3.NilpotentLieFiltration.squareRelative_same_diagonal_mod_kernel line 130