OAI/LinearAlgebra/CliffordAlgebra/KugaSatake.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Rational even-Clifford operators, functorial transport, and their tensor forms in output-first order.

  1. theorem OAI.KugaSatake.sandwich_mem_even line 14
  2. def OAI.KugaSatake.cliffordOperator line 23
  3. theorem OAI.KugaSatake.cliffordOperator_apply line 38
  4. theorem OAI.KugaSatake.clifford_ι_injective line 42
  5. theorem OAI.KugaSatake.cliffordOperator_injective line 48
  6. theorem OAI.KugaSatake.vector_mul_inverse line 58
  7. theorem OAI.KugaSatake.inverse_mul_vector line 63
  8. def OAI.KugaSatake.changeRightFactor line 68
  9. theorem OAI.KugaSatake.changeRightFactor_coe line 73
  10. theorem OAI.KugaSatake.cliffordOperator_change_right line 77
  11. theorem OAI.KugaSatake.changeRightFactor_mul_reverse line 89
  12. def OAI.KugaSatake.changeRightUnit line 100
  13. theorem OAI.KugaSatake.cliffordMap_mem_even line 115
  14. def OAI.KugaSatake.evenCliffordMap line 130
  15. theorem OAI.KugaSatake.evenCliffordMap_coe line 140
  16. theorem OAI.KugaSatake.evenCliffordMap_operator line 144
  17. def OAI.KugaSatake.evenCliffordEquiv line 152
  18. def OAI.KugaSatake.tensorEndEquiv line 180
  19. theorem OAI.KugaSatake.tensorEndEquiv_tmul_apply line 185
  20. def OAI.KugaSatake.tensorForm line 188
  21. theorem OAI.KugaSatake.tensorForm_tensorEndEquiv line 194
  22. theorem OAI.KugaSatake.tensorEndEquiv_naturality line 205
  23. theorem OAI.KugaSatake.tensorForm_compression line 216
  24. theorem OAI.KugaSatake.tensorForm_postcomp line 228
  25. instance OAI.KugaSatake.clifford_finite line 249
  26. instance OAI.KugaSatake.evenClifford_finite line 253
  27. def OAI.KugaSatake.cliffordTensor line 257
  28. theorem OAI.KugaSatake.cliffordTensor_apply line 263
  29. theorem OAI.KugaSatake.cliffordTensor_injective line 269
  30. theorem OAI.KugaSatake.cliffordTensor_change_right line 275