OAI/Combinatorics/Progressions/Polynomial/RealSquarePolynomialFactors.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquarePolynomial_fst line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquarePolynomial_snd line 29
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquarePolynomial_adapted line 41
  4. theorem OAI.Erdos3.exists_bounded_realified_square_polynomial line 52
  5. def OAI.Erdos3.NilpotentLieFiltration.realSquareFstPolynomialHom line 93
  6. def OAI.Erdos3.NilpotentLieFiltration.realSquareSndPolynomialHom line 98
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareFstPolynomialHom_polynomial line 103
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareSndPolynomialHom_polynomial line 109
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realSquarePolynomial_ext line 115
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_realSquarePolynomial_lift line 136
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialMap_coefficient line 166
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelative_mem_iff_tensor line 174
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelative_polynomial_surjective line 189
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_normalized line 203
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient_of_polynomial line 211
  16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_normalizedRelative_preimage line 224
  17. theorem OAI.Erdos3.NilpotentLieFiltration.real_normalized_square_coefficient_identity line 252
  18. def OAI.Erdos3.NilpotentLieFiltration.realSquareDiagonalPolynomialHom line 288
  19. def OAI.Erdos3.NilpotentLieFiltration.realRelativeSquarePolynomial line 294
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareFstPolynomialHom_diagonal line 299
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareSndPolynomialHom_diagonal line 312
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareFstPolynomialHom_relative line 325
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareSndPolynomialHom_relative line 339
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realSquarePolynomial_factorization line 352
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareDifference_mem_two line 363
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realSquarePolynomial_horizontal line 369
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom_injective line 380