OAI/Combinatorics/Progressions/Estimates/FullMarkedNativeFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_marked_refiltered_factors line 24
  2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fractional_integral_constant_normalization line 95
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fractional_integral_polynomial_normalization line 111
  4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_prescribed_native_refiltered_factorization line 165
  5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_marked_target_normalization line 235
  6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_marked_native_factorization line 346
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fixed_marked_native_factorizations line 413