OAI/Analysis/IrrationalRotation/Operators/FiniteConvolutionAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantProjection.exists_nonzero_product_coeff_le line 11
2. theorem OAI.InvariantProjection.exists_nonzero_product_coeff_le_two_mul line 29