OAI/Analysis/TriangularHilbert/CyclicHomogeneity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.cyclicNorm line 11
2. lemma OAI.TriangularHilbert.cyclicKernelOutput_congr_ae line 14
3. lemma OAI.TriangularHilbert.cyclicMax_congr_ae line 26
4. lemma OAI.TriangularHilbert.cyclicNorm_congr_ae line 32
5. lemma OAI.TriangularHilbert.cyclicNorm_zero_left line 41
6. lemma OAI.TriangularHilbert.cyclicNorm_zero_right line 43
7. lemma OAI.TriangularHilbert.cyclicKernelOutput_smul line 46
8. lemma OAI.TriangularHilbert.cyclicMax_smul line 54
9. lemma OAI.TriangularHilbert.cyclicNorm_smul line 59