Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-15 04:56 9dd9b6b0

View on Github →

refactor(archive/imo/imo1969_q1): prove infinite statement, cleanup (#4391) The previous formalization didn't quite prove that there were infinitely many natural numbers with the desired property, but rather that for any natural number there's a larger one with the property. This PR changes the ending to prove that the set of integers described in the problem statement is infinite.

Estimated changes

added def a_choice
added theorem a_choice_good
added theorem a_choice_strict_mono
modified theorem factorization
added def good_nats
modified theorem imo1969_q1
modified theorem int_large
deleted theorem int_not_prime
modified theorem left_factor_large
added theorem not_prime_of_int_mul'
modified theorem polynomial_not_prime
modified theorem right_factor_large
added theorem strict_mono.nat_pow
modified theorem nat.factors_unique
added theorem nat.not_prime_mul'
modified theorem set.finite_Union
added theorem set.infinite_image_iff