OAI/Combinatorics/Progressions/Fourier/SharedFreeFactorizationFrequency.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_finite_refined_petal_vanish line 39
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_refined_petal_add_invariant line 67
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_corrected_common_petal_invariant line 96
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_corrected_common_petal_invariance line 133
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_corrected_orbit_petal_invariant line 206
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_affine_orbit_petal_invariant line 232