Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-22 04:34 61ccaf65

View on Github →

chore(*): fix various issues reported by sanity_check_mathlib (#1469)

  • chore(*): fix various issues reported by sanity_check_mathlib
  • Drop a misleading comment, fix the proof

Estimated changes

added theorem units.mk0_inj
deleted theorem units.units.mk0_inj
added theorem sub_sub_cancel
deleted def sub_sub_cancel
added theorem div_nonneg
deleted def div_nonneg
added theorem div_pos
deleted def div_pos
added theorem half_lt_self
deleted def half_lt_self
added theorem mul_equiv.map_mul
deleted def mul_equiv.map_mul
added theorem mul_equiv.map_one
deleted def mul_equiv.map_one
added theorem finsupp.lt_wf
deleted def finsupp.lt_wf
added theorem multiset.map_eq_zero
modified theorem mv_polynomial.degrees_neg
modified theorem mv_polynomial.degrees_sub
added def rat.{u}
deleted theorem rat.{u}
added theorem free_group.to_word.inj
added theorem free_group.to_word.mk
deleted theorem fin_dim_vectorspace_equiv
modified theorem imp_intro
added def not.elim
deleted theorem not.elim
modified theorem not_of_not_imp
added theorem poly.ext
deleted def poly.ext
added theorem poly.induction
deleted def poly.induction
added theorem poly.isp
deleted def poly.isp
modified theorem ideal.is_coprime_def
modified theorem ideal.is_coprime_self
modified theorem ideal.mem_span_pair
modified def ordinal.div_def
added theorem pgame.add_zero_equiv
added theorem pgame.zero_add_equiv
added theorem omega.coeffs.val_set
modified theorem tactic.ring.pow_add_rev