OAI/Algebra/FiniteTensor/ArtinSteps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Artin induction steps for distinguished and unit equations.

  1. theorem OAI.PD4Tensor.Spreading.seriesCoefficientMap_eq_algebraMap line 19
  2. theorem OAI.PD4Tensor.Spreading.aeval_map_square line 27
  3. theorem OAI.PD4Tensor.Spreading.option_artin_step line 40
  4. theorem OAI.PD4Tensor.Spreading.unit_artin_step line 93
  5. theorem OAI.PD4Tensor.Spreading.polynomial_remove_X_factor line 145