Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-07 01:58 2d6f88c2

View on Github →

chore: Add toml file for archive and counterexamples (#18388) The end goal here is to surface these in doc-gen. For doc-gen to behave these need to be mutually importable. A step is added to the "test" run that verifies this by trying to import everything at the same time. For this new test to pass, some files need namespaces wrapped around their content. Probably we should be more principled about this namespace wrapping, but that can be left as future work, as all we really care about to start integrating with doc-gen is avoiding clashes.

Estimated changes

deleted theorem Ico_lemma
deleted theorem b_le_b
deleted def bcubes
deleted theorem bottom_mem_side
deleted theorem cannot_cube_a_cube
deleted theorem correct.b_add_w_le_one
deleted theorem correct.nontrivial_fin
deleted theorem correct.side_subset
deleted theorem correct.w_ne_one
deleted theorem correct.zero_le_b
deleted theorem correct.zero_le_of_mem
deleted structure correct
deleted theorem cube.b_lt_xm
deleted theorem cube.b_mem_bottom
deleted theorem cube.b_mem_side
deleted theorem cube.b_mem_to_set
deleted theorem cube.b_ne_xm
deleted def cube.bottom
deleted theorem cube.head_shift_up
deleted theorem cube.hw'
deleted def cube.shift_up
deleted def cube.side
deleted theorem cube.side_nonempty
deleted theorem cube.side_tail
deleted theorem cube.side_unit_cube
deleted theorem cube.tail_shift_up
deleted def cube.to_set
deleted theorem cube.to_set_disjoint
deleted theorem cube.to_set_subset
deleted def cube.unit_cube
deleted theorem cube.univ_pi_side
deleted def cube.xm
deleted structure cube
deleted def decreasing_sequence
deleted theorem exists_mi
deleted def mi
deleted theorem mi_mem_bcubes
deleted theorem mi_minimal
deleted theorem mi_not_on_boundary'
deleted theorem mi_not_on_boundary
deleted theorem mi_strict_minimal
deleted theorem mi_xm_ne_one
deleted theorem nonempty_bcubes
deleted theorem nontrivial_bcubes
deleted theorem not_correct
deleted def on_boundary
deleted theorem smallest_on_boundary
deleted theorem t_le_t
deleted theorem tail_sub
deleted def valley
deleted theorem valley_mi
deleted theorem valley_unit_cube
deleted theorem w_lt_w
added theorem «82».Ico_lemma
added theorem «82».b_le_b
added def «82».bcubes
added theorem «82».bottom_mem_side
added structure «82».correct
added theorem «82».cube.b_lt_xm
added theorem «82».cube.b_mem_side
added theorem «82».cube.b_ne_xm
added theorem «82».cube.hw'
added def «82».cube.side
added theorem «82».cube.side_tail
added def «82».cube.xm
added structure «82».cube
added theorem «82».exists_mi
added def «82».mi
added theorem «82».mi_mem_bcubes
added theorem «82».mi_minimal
added theorem «82».mi_xm_ne_one
added theorem «82».nonempty_bcubes
added theorem «82».not_correct
added theorem «82».t_le_t
added theorem «82».tail_sub
added def «82».valley
added theorem «82».valley_mi
added theorem «82».w_lt_w
deleted theorem ge_100
added theorem imo1960_q1.ge_100
added theorem imo1960_q1.lt_1000
added theorem imo1960_q1.not_zero
deleted theorem left_direction
deleted theorem lt_1000
deleted theorem not_zero
deleted def problem_predicate
deleted theorem right_direction
deleted def search_up_to
deleted theorem search_up_to_end
deleted theorem search_up_to_start
deleted theorem search_up_to_step
deleted def solution_predicate
deleted def sum_of_squares
deleted theorem case_0_digit
deleted theorem case_1_digit
deleted theorem case_2_digit
deleted theorem case_3_digit
deleted theorem case_4_digit
deleted theorem case_5_digit
deleted theorem case_more_digits
deleted theorem helper_5_digit
deleted theorem no_smaller_solutions
deleted def problem_predicate'
deleted def problem_predicate
deleted theorem satisfied_by_153846
deleted theorem without_digits
deleted def a_choice
deleted theorem a_choice_good
deleted theorem a_choice_strict_mono
deleted theorem factorization
deleted def good_nats
added theorem imo1969_q1.int_large
deleted theorem int_large
deleted theorem left_factor_large
deleted theorem not_prime_of_int_mul'
deleted theorem polynomial_not_prime
deleted theorem right_factor_large