OAI/Analysis/IrrationalRotation/Rotation/RotationInjective.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.representation_operator_injective_of_orbit_nonzero line 9
  2. theorem OAI.Invariant233.Rotation.orbitWeight_nonzero_ae line 26
  3. theorem OAI.Invariant233.Rotation.representation_real_injective line 42
  4. theorem OAI.Invariant233.Rotation.weightedReal_injective line 48
  5. theorem OAI.Invariant233.Rotation.representation_real_ker_eq_bot line 53