OAI/Combinatorics/Progressions/Linear/VaryingRankFixedPatchFunction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialPatch.castRank line 13
2. theorem OAI.Erdos3.PolynomialPatch.castRank_value line 16
3. theorem OAI.Erdos3.PolynomialPatch.castRank_kernel_lip line 21
4. def OAI.Erdos3.PolynomialPatch.formAtWeight line 26
5. theorem OAI.Erdos3.PolynomialPatch.formAtWeight_value line 29
6. def OAI.Erdos3.PolynomialPatch.rankWeightCode line 35
7. theorem OAI.Erdos3.PolynomialPatch.rankWeightCode_eq line 40
8. theorem OAI.Erdos3.exists_patch_rank_weight_class line 54
9. theorem OAI.Erdos3.exists_common_rank_weight_patch_family line 83
10. theorem OAI.Erdos3.exists_varying_rank_fixed_patch_function line 134