OAI/Combinatorics/Progressions/Fourier/RealLayerHorizontalFrequency.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.realification_range line 11
2. theorem OAI.Erdos3.real_lieTreeEval_hom line 16
3. theorem OAI.Erdos3.DegreeRankLieFiltration.real_layerProjection_mem line 34
4. def OAI.Erdos3.DegreeRankLieFiltration.realLayerProjection line 40
5. theorem OAI.Erdos3.DegreeRankLieFiltration.real_layerHorizontalMap_component line 46
6. theorem OAI.Erdos3.DegreeRankLieFiltration.real_layerHorizontalImage_frequency line 62