OAI/Combinatorics/Progressions/Polynomial/RankPolynomialFactorization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasis_weight_pos line 18
  2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasis_weight_le_step line 24
  3. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_bracket line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_bracket_height line 54
  5. theorem OAI.Erdos3.NilpotentLieFiltration.symbolBasisIndex_degree_le line 81
  6. def OAI.Erdos3.NilpotentLieFiltration.symbolBasisCode line 87
  7. theorem OAI.Erdos3.NilpotentLieFiltration.symbolBasisCode_injective line 94
  8. theorem OAI.Erdos3.NilpotentLieFiltration.symbolBasisIndex_finite line 112
  9. def OAI.Erdos3.NilpotentLieFiltration.symbolBasisIndexFintype line 115
  10. theorem OAI.Erdos3.NilpotentLieFiltration.symbolBasisIndex_card_le line 119
  11. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbol_finiteDimensional line 142
  12. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbol_finrank_le line 148
  13. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolFiltration line 168
  14. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolFiltration_layer line 174
  15. abbrev OAI.Erdos3.NilpotentLieFiltration.AdaptedBasisIndex line 210
  16. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedMonomialBasis_bracket line 219
  17. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedMonomialBasis_bracket_height line 233
  18. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasisIndex_degree_le line 253
  19. def OAI.Erdos3.NilpotentLieFiltration.adaptedBasisCode line 259
  20. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasisCode_injective line 266
  21. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasisIndex_finite line 284
  22. def OAI.Erdos3.NilpotentLieFiltration.adaptedBasisIndexFintype line 287
  23. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedBasisIndex_card_le line 291
  24. theorem OAI.Erdos3.NilpotentLieFiltration.symbol_dimension_bound_le_power line 318
  25. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_bch_coordinate_budget line 331
  26. def OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitCoordinates line 394
  27. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitCoordinates_log line 407
  28. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitCoordinates_symm_log line 410
  29. def OAI.Erdos3.DegreeRankLieFiltration.rankCoefficientOrbitHom line 427
  30. theorem OAI.Erdos3.DegreeRankLieFiltration.rankCoefficientOrbitHom_eq_iff line 445
  31. theorem OAI.Erdos3.DegreeRankLieFiltration.rankCoefficientOrbitHom_eq_one_iff line 451
  32. theorem OAI.Erdos3.DegreeRankLieFiltration.polynomialOrbit_mul_coefficient_sub_mem_rank_two line 459
  33. theorem OAI.Erdos3.DegreeRankLieFiltration.exists_polynomialOrbit_factorization_rank_two line 482