Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-17 23:24 c83c28a1

View on Github →

feat(archive/imo): add IMO 2019 problem 4 (#4482)

Estimated changes

Created archive/imo/imo2019_q4.lean

added theorem imo2019_q4

added theorem imo2019_q4_upper_bound

Modified src/algebra/big_operators/default.lean

Created src/algebra/big_operators/enat.lean

added theorem finset.sum_nat_coe_enat

Modified src/data/int/basic.lean

added theorem int.exists_lt_and_lt_iff_not_dvd

Modified src/data/nat/basic.lean

added theorem nat.exists_lt_and_lt_iff_not_dvd

Modified src/data/nat/bitwise.lean

added theorem nat.bit_eq_zero

Modified src/data/nat/enat.lean

added def enat.coe_hom

Modified src/data/nat/multiplicity.lean

added theorem nat.multiplicity_two_factorial_lt

added theorem nat.prime.multiplicity_factorial_mul

added theorem nat.prime.multiplicity_factorial_mul_succ

modified theorem nat.prime.multiplicity_one

Modified src/order/basic.lean

added theorem monotone.ne_of_lt_of_lt_int

added theorem monotone.ne_of_lt_of_lt_nat