Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-15 20:26 74c25a57

View on Github →

feat(*): lemmas needed for two projects (#1294)

  • feat(multiplicity|enat): add facts needed for IMO 2019-4
  • feat(*): various lemmas needed for the cubing a cube proof
  • typo
  • some cleanup
  • fixes, add choose_two_right
  • projections for associated.prime and irreducible

Estimated changes

added theorem irreducible.ne_zero
added theorem irreducible.not_unit
deleted theorem ne_zero_of_irreducible
modified theorem not_prime_zero
added theorem pow_dvd_pow_iff
added theorem prime.div_or_div
added theorem prime.ne_zero
added theorem prime.not_unit
added theorem finset.prod_le_prod
added theorem finset.prod_nat_cast
added theorem finset.prod_nonneg
added theorem finset.prod_pos
added theorem add_le_iff_nonpos_left
added theorem add_lt_iff_neg_left
added theorem add_lt_iff_neg_right
added def fin.cons
added theorem fin.cons_succ
added theorem fin.cons_zero
added theorem fin.exists_fin_succ
added theorem fin.forall_fin_succ
added def fin.tail
added theorem fin.tail_cons
added theorem finset.exists_min
added theorem nat.choose_two_right
added theorem nat.fact_eq_one
added theorem nat.fact_inj
added theorem nat.fact_lt
added theorem nat.monotone_fact
added theorem nat.one_lt_fact
added theorem nat.triangle_succ
added theorem enat.add_one_le_iff_lt
added theorem enat.add_one_le_of_lt
added theorem enat.le_of_lt_add_one
added theorem enat.lt_add_one
added theorem enat.lt_add_one_iff_lt
added theorem enat.ne_top_iff
added theorem enat.ne_top_of_lt
added theorem enat.top_eq_none
added theorem roption.ne_none_iff
added theorem roption.some_ne_none
added theorem set.exists_min
added theorem set.eq_of_Ico_disjoint
added theorem set.nonempty_Ico_sdiff
added theorem set.not_disjoint_iff
added theorem reflect_lt