OAI/Algebra/FiniteTensor/SeparatedForms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Separated block forms and compatibility of differential and multiplication operators.

  1. def OAI.PD4Tensor.TruncatedForms.BlockCoords line 17
  2. instance OAI.PD4Tensor.TruncatedForms.blockFintype line 21
  3. instance OAI.PD4Tensor.TruncatedForms.blockDecEq line 29
  4. def OAI.PD4Tensor.TruncatedForms.separatedEquiv line 39
  5. theorem OAI.PD4Tensor.TruncatedForms.separatedEquiv_zero line 47
  6. theorem OAI.PD4Tensor.TruncatedForms.separatedEquiv_succ line 52
  7. theorem OAI.PD4Tensor.TruncatedForms.separatedEquiv_succ_tprod line 58
  8. theorem OAI.PD4Tensor.TruncatedForms.D_separated line 69
  9. theorem OAI.PD4Tensor.TruncatedForms.parity_product line 112
  10. theorem OAI.PD4Tensor.TruncatedForms.parity_separated line 120
  11. def OAI.PD4Tensor.TruncatedForms.separatedPotential line 154
  12. theorem OAI.PD4Tensor.TruncatedForms.koszul_separated line 163
  13. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_product line 212
  14. def OAI.PD4Tensor.TruncatedForms.separatedProduct line 224
  15. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_separated line 236