OAI/Combinatorics/Progressions/Linear/KernelProjectionPresentPivotIdeal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.KernelProjectionPresentPivot line 13
  2. instance OAI.Erdos3.(instance at line 16) line 16
  3. def OAI.Erdos3.kernelProjectionSelectedPivot line 19
  4. theorem OAI.Erdos3.kernelProjectionSelectedPivot_spec line 23
  5. theorem OAI.Erdos3.kernelProjectionPresentPivot_card_le line 27
  6. def OAI.Erdos3.kernelProjectionLocalPivotTests line 37
  7. theorem OAI.Erdos3.exists_kernel_projection_fixed_native_partners line 42
  8. theorem OAI.Erdos3.exists_external_kernel_pivot_masks line 111
  9. theorem OAI.Erdos3.finiteFrequencyKernel_presentPivots line 183
  10. theorem OAI.Erdos3.NilpotentLieFiltration.pivotAnnihilatorIdeal_presentPivots_toSubmodule line 209
  11. theorem OAI.Erdos3.NilpotentLieFiltration.pivotAnnihilatorIdeal_presentPivots line 216