OAI/Algebra/FiniteTensor/TensorResidues.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Three-block cycles, Frobenius residues and nonzero normal pairings.

  1. def OAI.PD4Tensor.TruncatedForms.sigmaBlock line 20
  2. def OAI.PD4Tensor.TruncatedForms.sigmaSelected line 23
  3. theorem OAI.PD4Tensor.TruncatedForms.sigmaPotential_single line 28
  4. theorem OAI.PD4Tensor.TruncatedForms.koszul_sigmaBlock line 37
  5. theorem OAI.PD4Tensor.TruncatedForms.sigmaProduct_selected line 58
  6. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_sigmaSelected line 65
  7. theorem OAI.PD4Tensor.TruncatedForms.exists_three_tensor_form_cycle line 94
  8. def OAI.PD4Tensor.FrobeniusTruncation.socle line 193
  9. theorem OAI.PD4Tensor.FrobeniusTruncation.residue_socle_product line 196
  10. def OAI.PD4Tensor.FrobeniusTruncation.linearForm line 211
  11. theorem OAI.PD4Tensor.FrobeniusTruncation.linearForm_constant line 215
  12. def OAI.PD4Tensor.FrobeniusTruncation.linearSubst line 220
  13. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_coord line 234
  14. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_mul line 247
  15. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_diagonal_coord line 258
  16. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_transvection_coord line 262
  17. theorem OAI.PD4Tensor.FrobeniusTruncation.add_pow_mul_eq line 275
  18. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_transvection_socle line 286
  19. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_socle line 311
  20. theorem OAI.PD4Tensor.FrobeniusTruncation.high_augmentation_le line 326
  21. def OAI.PD4Tensor.FrobeniusTruncation.linearPart line 353
  22. theorem OAI.PD4Tensor.FrobeniusTruncation.coeff_linearPart line 356
  23. theorem OAI.PD4Tensor.FrobeniusTruncation.linearPart_constant line 375
  24. theorem OAI.PD4Tensor.FrobeniusTruncation.mem_augmentation line 380
  25. theorem OAI.PD4Tensor.FrobeniusTruncation.sub_linearPart_mem line 390
  26. theorem OAI.PD4Tensor.FrobeniusTruncation.filtered_pow_sub line 402
  27. theorem OAI.PD4Tensor.FrobeniusTruncation.filtered_prod_mem line 419
  28. theorem OAI.PD4Tensor.FrobeniusTruncation.filtered_prod_sub line 431
  29. theorem OAI.PD4Tensor.FrobeniusTruncation.top_product_eq_linear line 461
  30. theorem OAI.PD4Tensor.FrobeniusTruncation.coord_mul_socle line 482
  31. theorem OAI.PD4Tensor.FrobeniusTruncation.mk_mul_socle line 491
  32. def OAI.PD4Tensor.FrobeniusTruncation.tangentMatrix line 506
  33. theorem OAI.PD4Tensor.FrobeniusTruncation.top_product_eq_socle line 511
  34. def OAI.PD4Tensor.FrobeniusTruncation.jacobianDet line 530
  35. theorem OAI.PD4Tensor.FrobeniusTruncation.constantCoeff_pderiv line 534
  36. theorem OAI.PD4Tensor.FrobeniusTruncation.jacobianDet_constant line 541
  37. theorem OAI.PD4Tensor.FrobeniusTruncation.normal_residue line 555
  38. theorem OAI.PD4Tensor.FrobeniusTruncation.normal_residue_ne_zero line 565