OAI/Algebra/FiniteTensor/FrobeniusQuotient.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Frobenius quotients, bounded coefficients, residues and derivatives.

  1. def OAI.PD4Tensor.FrobeniusTruncation.ideal line 16
  2. abbrev OAI.PD4Tensor.FrobeniusTruncation.Ring line 19
  3. def OAI.PD4Tensor.FrobeniusTruncation.coord line 21
  4. theorem OAI.PD4Tensor.FrobeniusTruncation.variable_pow line 25
  5. theorem OAI.PD4Tensor.FrobeniusTruncation.ideal_as_monomials line 30
  6. def OAI.PD4Tensor.FrobeniusTruncation.socleExponent line 44
  7. theorem OAI.PD4Tensor.FrobeniusTruncation.socleExponent_apply line 47
  8. theorem OAI.PD4Tensor.FrobeniusTruncation.coeff_zero_of_mem_ideal line 52
  9. def OAI.PD4Tensor.FrobeniusTruncation.residue line 61
  10. theorem OAI.PD4Tensor.FrobeniusTruncation.residue_mk line 69
  11. theorem OAI.PD4Tensor.FrobeniusTruncation.residue_socle line 73
  12. theorem OAI.PD4Tensor.FrobeniusTruncation.socle_ne_zero line 79
  13. theorem OAI.PD4Tensor.FrobeniusTruncation.pderiv_mem line 90
  14. def OAI.PD4Tensor.FrobeniusTruncation.derivative line 107
  15. theorem OAI.PD4Tensor.FrobeniusTruncation.derivative_mk line 117
  16. theorem OAI.PD4Tensor.FrobeniusTruncation.residue_derivative line 123
  17. theorem OAI.PD4Tensor.FrobeniusTruncation.derivative_mul line 132
  18. theorem OAI.PD4Tensor.FrobeniusTruncation.polynomial_pderiv_commute line 141
  19. theorem OAI.PD4Tensor.FrobeniusTruncation.derivative_commute line 156
  20. theorem OAI.PD4Tensor.FrobeniusTruncation.frobenius_mk line 166