OAI/Algebra/FiniteTensor/NilpotentSubstitution.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Algebraicity of full nilpotent substitution and the scalar equation systems.

  1. abbrev OAI.PD4Tensor.Spreading.SeriesFraction line 16
  2. def OAI.PD4Tensor.Spreading.seriesFractionParameters line 18
  3. theorem OAI.PD4Tensor.Spreading.boxCoeff_seriesFractionParameters line 23
  4. theorem OAI.PD4Tensor.Spreading.augmentation_seriesFractionParameters line 29
  5. theorem OAI.PD4Tensor.Spreading.seriesFractionParameters_map line 35
  6. theorem OAI.PD4Tensor.Spreading.map_augmentation_map line 42
  7. def OAI.PD4Tensor.Spreading.nilSubstitution line 55
  8. theorem OAI.PD4Tensor.Spreading.nilSubstitution_apply line 61
  9. theorem OAI.PD4Tensor.Spreading.augmentation_nilSubstitution line 68
  10. theorem OAI.PD4Tensor.Spreading.nilSubstitution_C line 82
  11. theorem OAI.PD4Tensor.Spreading.nilSubstitution_X line 90
  12. theorem OAI.PD4Tensor.Spreading.algebraic_constant_series line 102
  13. theorem OAI.PD4Tensor.Spreading.algebraic_series_fraction_iff line 109
  14. theorem OAI.PD4Tensor.Spreading.algebraic_box_subst line 117
  15. def OAI.PD4Tensor.Spreading.algebraicBoxRing line 203
  16. theorem OAI.PD4Tensor.Spreading.mem_algebraicBoxRing line 208
  17. theorem OAI.PD4Tensor.Spreading.boxSeries_C line 223
  18. theorem OAI.PD4Tensor.Spreading.C_mem_algebraicBoxRing line 230
  19. theorem OAI.PD4Tensor.Spreading.map_mem_algebraicBoxRing line 240
  20. theorem OAI.PD4Tensor.Spreading.assembleBox_mem_algebraicBoxRing line 252
  21. theorem OAI.PD4Tensor.Spreading.boxSeries_pderiv line 260
  22. theorem OAI.PD4Tensor.Spreading.pderiv_mem_algebraicBoxRing line 269
  23. theorem OAI.PD4Tensor.Spreading.subst_mem_algebraicBoxRing line 278
  24. theorem OAI.PD4Tensor.Spreading.algebraic_variable_series line 307
  25. theorem OAI.PD4Tensor.Spreading.algebraic_affineUnknown line 314
  26. theorem OAI.PD4Tensor.Spreading.algebraic_series_sum line 321
  27. theorem OAI.PD4Tensor.Spreading.map_augmentation_eq_boxSeries_zero line 332
  28. theorem OAI.PD4Tensor.Spreading.algebraic_potential line 344
  29. theorem OAI.PD4Tensor.Spreading.algebraic_perturbation line 353
  30. theorem OAI.PD4Tensor.Spreading.deformed_mem_algebraicBoxRing line 360
  31. theorem OAI.PD4Tensor.Spreading.universalLeftH_mem_algebraicBoxRing line 372
  32. theorem OAI.PD4Tensor.Spreading.universalLeftP_mem_algebraicBoxRing line 377
  33. def OAI.PD4Tensor.Spreading.leftCentralEmbedding line 381
  34. theorem OAI.PD4Tensor.Spreading.augmentation_universalLeftH line 386
  35. theorem OAI.PD4Tensor.Spreading.universalLeft_substitution_algebraic line 397
  36. theorem OAI.PD4Tensor.Spreading.universalRightG_eq_X line 407
  37. theorem OAI.PD4Tensor.Spreading.universalRight_substitution_algebraic line 412
  38. theorem OAI.PD4Tensor.Spreading.universalLeftEquation_algebraic line 424
  39. theorem OAI.PD4Tensor.Spreading.universalRightP_algebraic line 441
  40. theorem OAI.PD4Tensor.Spreading.universalRightSummand_algebraic line 448
  41. theorem OAI.PD4Tensor.Spreading.universalRightEquation_algebraic line 459