OAI/Combinatorics/Progressions/Dynamics/RestrictedGradePathMembership.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.reset_splitting_in_quotient line 10
  2. theorem OAI.Erdos3.NilpotentLieFiltration.reset_real_splitting line 30
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_reset_bounds line 69
  4. abbrev OAI.Erdos3.NilpotentLieFiltration.RealSymbolGradeQuotientGroup line 178
  5. def OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientHom line 185
  6. theorem OAI.Erdos3.NilpotentLieFiltration.reset_real_symbol_splitting line 189
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_reset line 226
  8. theorem OAI.Erdos3.VectorPolynomial.coefficients_realChartSubstitute_mem_of_range line 281
  9. theorem OAI.Erdos3.NilpotentLieFiltration.restricted_grade_path_coefficients line 300
  10. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol_mem_of_grade_values line 315
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotient_mem_of_grade_values line 330
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotient_mem_of_restricted_path line 344