OAI/Algebra/FiniteTensor/GermBranches.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Jet stability of algebraic branches, coordinate removal and constant coefficients.

  1. theorem OAI.PD4Tensor.Spreading.polynomial_root_equal_of_jet line 17
  2. theorem OAI.PD4Tensor.Spreading.polynomial_eval₂_congr_ideal line 37
  3. theorem OAI.PD4Tensor.Spreading.polynomial_moving_branch line 52
  4. theorem OAI.PD4Tensor.Spreading.truncTotal_eq_of_close line 81
  5. theorem OAI.PD4Tensor.Spreading.close_of_truncTotal_eq line 90
  6. theorem OAI.PD4Tensor.Spreading.subst_close_jet line 100
  7. theorem OAI.PD4Tensor.Spreading.aeval_relation_subst line 124
  8. theorem OAI.PD4Tensor.Spreading.germ_branch_stability line 148
  9. theorem OAI.PD4Tensor.Spreading.algebraic_constantCoeff line 186
  10. theorem OAI.PD4Tensor.Spreading.algebraic_optionEquiv line 247
  11. theorem OAI.PD4Tensor.Spreading.algebraic_drop_option line 262
  12. theorem OAI.PD4Tensor.Spreading.algebraic_rename_equiv line 278
  13. theorem OAI.PD4Tensor.Spreading.killCompl_comp_apply line 290
  14. theorem OAI.PD4Tensor.Spreading.killCompl_equiv line 296
  15. theorem OAI.PD4Tensor.Spreading.drop_ne_eq_killCompl line 304
  16. theorem OAI.PD4Tensor.Spreading.algebraic_drop_ne line 324
  17. theorem OAI.PD4Tensor.Spreading.algebraic_killCompl line 334