OAI/Analysis/IrrationalRotation/Rotation/WeightedShiftAlgebra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.WeightedShift.diagonalAlgHom_apply line 10
  2. theorem OAI.Invariant233.WeightedShift.diagonal_one line 12
  3. theorem OAI.Invariant233.WeightedShift.diagonal_zero line 13
  4. theorem OAI.Invariant233.WeightedShift.diagonal_add line 14
  5. theorem OAI.Invariant233.WeightedShift.diagonal_mul line 16
  6. theorem OAI.Invariant233.WeightedShift.diagonal_smul line 18
  7. theorem OAI.Invariant233.WeightedShift.diagonal_star line 21
  8. theorem OAI.Invariant233.WeightedShift.translate_apply line 32
  9. theorem OAI.Invariant233.WeightedShift.translate_zero line 34
  10. theorem OAI.Invariant233.WeightedShift.translate_add line 38
  11. theorem OAI.Invariant233.WeightedShift.diagonal_shift_covariance line 43
  12. theorem OAI.Invariant233.WeightedShift.shift_add line 50
  13. theorem OAI.Invariant233.WeightedShift.shift_zero line 58
  14. theorem OAI.Invariant233.WeightedShift.conjugate_diagonal line 63
  15. theorem OAI.Invariant233.WeightedShift.diagonal_injective line 69