OAI/Algebra/FiniteTensor/FormalEvaluation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent formal evaluation and bijective formal substitutions.

  1. def OAI.PD4Tensor.nilEval line 18
  2. theorem OAI.PD4Tensor.nilEval_X line 25
  3. theorem OAI.PD4Tensor.nilEval_coe line 34
  4. theorem OAI.PD4Tensor.nilEval_map line 43
  5. theorem OAI.PD4Tensor.nilEval_nilpotent line 58
  6. theorem OAI.PD4Tensor.nilEval_subst line 73
  7. theorem OAI.PD4Tensor.continuous_formal_pderiv line 93
  8. theorem OAI.PD4Tensor.nilEval_pderiv_coe line 103
  9. theorem OAI.PD4Tensor.nilEval_pderiv line 120
  10. def OAI.PD4Tensor.FrobeniusTruncation.boundedCoeff line 147
  11. theorem OAI.PD4Tensor.FrobeniusTruncation.boundedCoeff_mk line 153
  12. def OAI.PD4Tensor.FrobeniusTruncation.formalEval line 157
  13. theorem OAI.PD4Tensor.FrobeniusTruncation.formalEval_coe line 161
  14. theorem OAI.PD4Tensor.FrobeniusTruncation.boundedCoeff_formalEval line 175
  15. theorem OAI.PD4Tensor.FrobeniusTruncation.formalEval_pow line 194
  16. def OAI.PD4Tensor.FrobeniusTruncation.formalSubst line 203
  17. theorem OAI.PD4Tensor.FrobeniusTruncation.formalSubst_coord line 211
  18. theorem OAI.PD4Tensor.FrobeniusTruncation.formalSubst_bijective line 219