OAI/Combinatorics/Progressions/Polynomial/CurrentPolynomialDerivativeRemoval.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystem line 14
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystem.remove line 18
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystem.real_evaluation line 26
  4. theorem OAI.Erdos3.NilpotentLieFiltration.formal_current_layer_correction_preserves_lifts line 41
  5. def OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystemMod line 76
  6. def OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystemMod line 80
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystem.to_mod line 84
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystem.to_mod line 91
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystemMod.exact_left line 99
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystemMod.exact_system line 105
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystemMod.remove line 117
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialDerivativeSystemMod.remove line 129
  13. theorem OAI.Erdos3.NilpotentLieFiltration.polynomial_grade_eq_of_sub_mem_next line 170
  14. theorem OAI.Erdos3.NilpotentLieFiltration.polynomial_grade_adjoint_eq line 184
  15. theorem OAI.Erdos3.NilpotentLieFiltration.polynomial_grade_logDerivative_eq line 194
  16. theorem OAI.Erdos3.NilpotentLieFiltration.current_derivative_removal_projection line 224
  17. theorem OAI.Erdos3.NilpotentLieFiltration.current_derivative_defect_preserved line 254