OAI/Combinatorics/Progressions/Polynomial/PrescribedFastPolynomialFactorization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientLinear line 18
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientLinear_map line 26
  3. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientHom line 31
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientHom_bijective line 42
  5. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientEquiv line 54
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientEquiv_map line 59
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_polynomial_normalization line 75
  8. theorem OAI.Erdos3.exists_native_polynomial_normalization line 116
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolQuotientEquiv_natural line 169
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_polynomial_lift_with_symbol line 180
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_polynomial_group_lift_with_symbol line 210
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_prescribed_marked_polynomial_factorization line 244
  13. def OAI.Erdos3.NilpotentLieFiltration.realFilteredSymbolGroupMap line 288
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_prescribed_fast_polynomial_factorization line 295