OAI/Algebra/FiniteTensor/NilpotentRoots.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Parameter-series equivalences, nilpotent root lifting and algebraic descent.

  1. def OAI.PD4Tensor.Spreading.parametersToSeries line 19
  2. theorem OAI.PD4Tensor.Spreading.parametersToSeries_algebraMap line 33
  3. theorem OAI.PD4Tensor.Spreading.parametersToSeries_parameter line 39
  4. theorem OAI.PD4Tensor.Spreading.parametersToSeries_boxMonomial line 45
  5. theorem OAI.PD4Tensor.Spreading.parametersToSeries_eq_assemble line 54
  6. theorem OAI.PD4Tensor.Spreading.boxSeries_parametersToSeries line 64
  7. theorem OAI.PD4Tensor.Spreading.parametersToSeries_bijective line 68
  8. def OAI.PD4Tensor.Spreading.seriesParameterEquiv line 86
  9. theorem OAI.PD4Tensor.Spreading.boxCoeff_seriesParameterEquiv line 89
  10. theorem OAI.PD4Tensor.Spreading.seriesParameterEquiv_map line 95
  11. theorem OAI.PD4Tensor.Spreading.augmentation_eq_boxCoeff_zero line 102
  12. theorem OAI.PD4Tensor.Spreading.augmentation_seriesParameterEquiv line 110
  13. theorem OAI.PD4Tensor.Spreading.root_lift_nilpotent line 127
  14. theorem OAI.PD4Tensor.Spreading.root_unique_nilpotent line 181
  15. theorem OAI.PD4Tensor.Spreading.parameterIdeal_nilpotent line 203
  16. theorem OAI.PD4Tensor.Spreading.parameter_sub_constant_mem line 207
  17. theorem OAI.PD4Tensor.Spreading.parameter_mem_iff_augmentation_zero line 222
  18. theorem OAI.PD4Tensor.Spreading.parameter_isUnit_of_augmentation line 234
  19. theorem OAI.PD4Tensor.Spreading.squarefree_root_descent line 243
  20. def OAI.PD4Tensor.Spreading.algebraicSubfield line 298
  21. theorem OAI.PD4Tensor.Spreading.mem_algebraicSubfield line 307
  22. theorem OAI.PD4Tensor.Spreading.exists_parameter_lift line 312
  23. theorem OAI.PD4Tensor.Spreading.mem_parameter_range line 325
  24. def OAI.PD4Tensor.Spreading.parameterRangeEquiv line 333
  25. def OAI.PD4Tensor.Spreading.liftParametersHom line 341
  26. theorem OAI.PD4Tensor.Spreading.map_liftParametersHom line 347
  27. theorem OAI.PD4Tensor.Spreading.squarefree_root_algebraic line 354