OAI/Analysis/Cotype/ProjectionSpectrum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.projectionPattern line 10
2. theorem OAI.Cotype.projectionProduct_pointwise_mul line 13
3. theorem OAI.Cotype.projectionProduct_zero_of_factor line 26
4. theorem OAI.Cotype.projectionPattern_factor_commute line 38
5. theorem OAI.Cotype.projectionPattern_mul line 50
6. theorem OAI.Cotype.projectionPattern_sum line 75
7. theorem OAI.Cotype.projectionSemigroup_pattern_expansion line 81