OAI/Algebra/FiniteTensor/LinearCharts.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Regular linear charts and polynomial compatibility of coordinate changes.

  1. theorem OAI.PD4Tensor.Spreading.totalDegree_eval₂_linear line 17
  2. theorem OAI.PD4Tensor.Spreading.coe_eval₂_polynomials line 38
  3. theorem OAI.PD4Tensor.Spreading.exists_nonzero_line line 54
  4. def OAI.PD4Tensor.Spreading.linearChartVars line 124
  5. theorem OAI.PD4Tensor.Spreading.linearChartVars_const line 128
  6. theorem OAI.PD4Tensor.Spreading.linearChartVars_hasSubst line 132
  7. theorem OAI.PD4Tensor.Spreading.linearChartVars_comp line 135
  8. def OAI.PD4Tensor.Spreading.inverseChartPoint line 149
  9. theorem OAI.PD4Tensor.Spreading.chart_inverse_relations line 153
  10. def OAI.PD4Tensor.Spreading.linearSeriesChart line 164
  11. theorem OAI.PD4Tensor.Spreading.linearSeriesChart_apply line 187
  12. def OAI.PD4Tensor.Spreading.axisVars line 191
  13. theorem OAI.PD4Tensor.Spreading.axisVars_hasSubst line 193
  14. theorem OAI.PD4Tensor.Spreading.axisVars_subst_linearChartVars line 196
  15. theorem OAI.PD4Tensor.Spreading.axis_linearSeriesChart line 206
  16. theorem OAI.PD4Tensor.Spreading.exists_regular_linear_chart line 223
  17. theorem OAI.PD4Tensor.Spreading.series_equiv_jet line 247
  18. def OAI.PD4Tensor.Spreading.polynomialChartVars line 261
  19. def OAI.PD4Tensor.Spreading.polynomialChart line 265
  20. theorem OAI.PD4Tensor.Spreading.polynomialChart_square line 268
  21. theorem OAI.PD4Tensor.Spreading.polynomialChart_injective line 282
  22. theorem OAI.PD4Tensor.Spreading.algebraic_linearSeriesChart line 296
  23. theorem OAI.PD4Tensor.Spreading.linearSeriesChart_symm_apply line 302
  24. theorem OAI.PD4Tensor.Spreading.algebraic_linearSeriesChart_symm line 307
  25. def OAI.PD4Tensor.Spreading.axisEmbedding line 322
  26. theorem OAI.PD4Tensor.Spreading.axis_subst_eq_killCompl line 324
  27. theorem OAI.PD4Tensor.Spreading.option_axis_constant line 352
  28. theorem OAI.PD4Tensor.Spreading.option_axis_rename line 367
  29. theorem OAI.PD4Tensor.Spreading.residue_regular_of_constant_regular line 387