OAI/NumberTheory/Ostmann/Supply/TensorModes.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Supply.TensorModes.augmentedSpace line 12
  2. def OAI.Ostmann.Supply.TensorModes.scalarPart line 15
  3. def OAI.Ostmann.Supply.TensorModes.centeredPart line 19
  4. theorem OAI.Ostmann.Supply.TensorModes.scalarPart_apply line 22
  5. theorem OAI.Ostmann.Supply.TensorModes.centeredPart_apply line 25
  6. theorem OAI.Ostmann.Supply.TensorModes.scalarPart_star line 31
  7. theorem OAI.Ostmann.Supply.TensorModes.centeredPart_star line 42
  8. theorem OAI.Ostmann.Supply.TensorModes.scalar_centered_mul line 45
  9. theorem OAI.Ostmann.Supply.TensorModes.centered_scalar_mul line 48
  10. theorem OAI.Ostmann.Supply.TensorModes.scalar_add_centered line 51
  11. theorem OAI.Ostmann.Supply.TensorModes.tensorOp_congr line 54
  12. theorem OAI.Ostmann.Supply.TensorModes.tensorOp_mul line 63
  13. theorem OAI.Ostmann.Supply.TensorModes.tensorOp_one line 73
  14. theorem OAI.Ostmann.Supply.TensorModes.tensorOp_adjoint line 82
  15. theorem OAI.Ostmann.Supply.TensorModes.tensorOp_zero_of_factor line 92
  16. def OAI.Ostmann.Supply.TensorModes.exactMode line 104
  17. theorem OAI.Ostmann.Supply.TensorModes.exactMode_star line 109
  18. theorem OAI.Ostmann.Supply.TensorModes.exactMode_mul_eq_zero line 125
  19. def OAI.Ostmann.Supply.TensorModes.retainedModes line 139
  20. def OAI.Ostmann.Supply.TensorModes.lowModes line 142
  21. theorem OAI.Ostmann.Supply.TensorModes.sum_exactMode_star line 147
  22. theorem OAI.Ostmann.Supply.TensorModes.lowModes_star line 160