OAI/Analysis/IrrationalRotation/Model/ProductCharacters.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InvariantProjection.ProductRotation.characterPhaseline 10 - def
OAI.InvariantProjection.ProductRotation.productCharacterline 14 - def
OAI.InvariantProjection.ProductRotation.productFourierAlgebraline 23