Commit 2022-08-15 23:11 1e6b748c

View on Github →

chore(combinatorics/*): Fix lint (#16031) Fix the linting errors coming from fintype_finite, to_additive_doc and doc_blame. Pull out a [projective_plane P L] assumption to a variables declaration in combinatorics.configuration.

Estimated changes

Modified src/combinatorics/additive/salem_spencer.lean

Modified src/combinatorics/configuration.lean

modified theorem configuration.projective_plane.card_lines

modified theorem configuration.projective_plane.card_points

modified theorem configuration.projective_plane.card_points_eq_card_lines

modified theorem configuration.projective_plane.dual.order

modified theorem configuration.projective_plane.line_count_eq

modified theorem configuration.projective_plane.line_count_eq_line_count

modified theorem configuration.projective_plane.line_count_eq_point_count

modified theorem configuration.projective_plane.one_lt_order

modified theorem configuration.projective_plane.point_count_eq

modified theorem configuration.projective_plane.point_count_eq_point_count

modified theorem configuration.projective_plane.two_lt_line_count

modified theorem configuration.projective_plane.two_lt_point_count

Modified src/combinatorics/hales_jewett.lean

modified theorem combinatorics.exists_mono_homothetic_copy

modified theorem combinatorics.line.exists_mono_in_high_dimension

Modified src/combinatorics/hall/finite.lean

Modified src/combinatorics/hindman.lean

Modified src/combinatorics/simple_graph/coloring.lean

modified theorem simple_graph.clique_free_of_chromatic_number_lt

modified theorem simple_graph.colorable_chromatic_number_of_fintype

added theorem simple_graph.coloring.color_classes_finite

deleted theorem simple_graph.coloring.color_classes_finite_of_fintype

modified theorem simple_graph.is_clique.card_le_chromatic_number

modified theorem simple_graph.is_empty_of_chromatic_number_eq_zero

Modified src/combinatorics/simple_graph/partition.lean

Modified src/data/setoid/partition.lean

added theorem setoid.finite_classes_ker

deleted theorem setoid.nonempty_fintype_classes_ker