OAI/Combinatorics/Progressions/Linear/RefilteredKernelConstantBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realificationLieHom_layer_surjective line 19
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realificationLieHom_top_kernel_eq_zero line 38
  3. theorem OAI.Erdos3.realification_fractional_integer_split line 73
  4. theorem OAI.Erdos3.exists_fractional_integer_kernel_correction line 96
  5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_kernel_constant_factors line 132
  6. theorem OAI.Erdos3.scalarExtension_coordinate_sum line 192
  7. theorem OAI.Erdos3.scalarExtension_fractional_coordinates_bound line 201
  8. theorem OAI.Erdos3.integral_basis_image_denominatorGrid line 221
  9. theorem OAI.Erdos3.integral_basis_image_realDenominatorGrid line 241
  10. theorem OAI.Erdos3.exists_basis_image_bounds_of_height line 250
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_kernel_constant_factors_with_bounds line 271