OAI/Combinatorics/Progressions/Estimates/NativeOptionPivotQuotientStrong.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.optionPivotProductQuotientMap line 21
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPivotProductQuotientMap_fst line 27
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPivotProductQuotientMap_snd line 32
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPivotProductQuotientMap_mem_layer line 38
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPivotProductQuotientMap_layer_surjective line 48
  6. def OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast line 67
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonFastTop_quotient_le line 83
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast_layer_eq line 116
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast_graded line 131
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast_top_le line 143
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast_top_kernel_eq_zero line 154
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionCommonPivotQuotientFast_graded_top_kernel line 167
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_optionCommonPivotQuotient_family_symbol_factors line 215
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonFastTop_quotient_kernel_eq_zero line 305
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast_top_kernel_eq_zero line 355
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast_graded_top_kernel line 370
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMarkedMap_mem_layer line 393
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast_graded_top_kernel_option line 418
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMarkedMap_layer_surjective line 463
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMarkedMap_surjective line 493
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMarkedMap_layer_map line 506
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMarkedMap_real_layer_surjective line 522