Commit 2022-09-04 16:26 d354c0d1

View on Github →

feat: depend on std4 (#397)

Estimated changes

deleted def Array.flatten
deleted def Array.ofFn
deleted def Array.range
deleted def Array.reduceOption
deleted theorem Nat.coprime.eq_one_of_dvd
deleted theorem Nat.coprime.gcd_both
deleted theorem Nat.coprime.gcd_eq_one
deleted theorem Nat.coprime.gcd_left
deleted theorem Nat.coprime.gcd_mul
deleted theorem Nat.coprime.gcd_right
deleted theorem Nat.coprime.mul
deleted theorem Nat.coprime.mul_right
deleted theorem Nat.coprime.pow
deleted theorem Nat.coprime.pow_left
deleted theorem Nat.coprime.pow_right
deleted theorem Nat.coprime.symm
deleted def Nat.coprime
deleted theorem Nat.coprime_comm
deleted theorem Nat.coprime_mul_iff_left
deleted theorem Nat.coprime_mul_iff_right
deleted theorem Nat.coprime_one_left
deleted theorem Nat.coprime_one_left_iff
deleted theorem Nat.coprime_one_right
deleted theorem Nat.coprime_one_right_iff
deleted theorem Nat.coprime_self
deleted theorem Nat.coprime_zero_left
deleted theorem Nat.coprime_zero_right
deleted theorem Nat.dvd_gcd
deleted theorem Nat.dvd_gcd_iff
deleted theorem Nat.dvd_lcm_left
deleted theorem Nat.dvd_lcm_right
deleted theorem Nat.exists_coprime'
deleted theorem Nat.exists_coprime
deleted theorem Nat.gcd.induction
deleted theorem Nat.gcd_add_mul_self
deleted theorem Nat.gcd_assoc
deleted theorem Nat.gcd_comm
deleted theorem Nat.gcd_div
deleted theorem Nat.gcd_dvd
deleted theorem Nat.gcd_dvd_gcd_mul_left
deleted theorem Nat.gcd_dvd_gcd_mul_right
deleted theorem Nat.gcd_dvd_left
deleted theorem Nat.gcd_dvd_right
deleted theorem Nat.gcd_eq_left
deleted theorem Nat.gcd_eq_left_iff_dvd
deleted theorem Nat.gcd_eq_right
deleted theorem Nat.gcd_eq_right_iff_dvd
deleted theorem Nat.gcd_eq_zero_iff
deleted theorem Nat.gcd_le_left
deleted theorem Nat.gcd_le_right
deleted theorem Nat.gcd_mul_dvd_mul_gcd
deleted theorem Nat.gcd_mul_lcm
deleted theorem Nat.gcd_mul_left
deleted theorem Nat.gcd_mul_left_left
deleted theorem Nat.gcd_mul_left_right
deleted theorem Nat.gcd_mul_right
deleted theorem Nat.gcd_mul_right_left
deleted theorem Nat.gcd_mul_right_right
deleted theorem Nat.gcd_one_right
deleted theorem Nat.gcd_pos_of_pos_left
deleted theorem Nat.gcd_pos_of_pos_right
deleted theorem Nat.gcd_rec
deleted def Nat.lcm
deleted theorem Nat.lcm_assoc
deleted theorem Nat.lcm_comm
deleted theorem Nat.lcm_dvd
deleted theorem Nat.lcm_ne_zero
deleted theorem Nat.lcm_one_left
deleted theorem Nat.lcm_one_right
deleted theorem Nat.lcm_self
deleted theorem Nat.lcm_zero_left
deleted theorem Nat.lcm_zero_right
modified theorem List.length_take_le
deleted theorem Nat.add_div_left
deleted theorem Nat.add_div_right
deleted theorem Nat.add_mod
deleted theorem Nat.add_mod_left
deleted theorem Nat.add_mod_mod
deleted theorem Nat.add_mod_right
deleted theorem Nat.add_mul_div_left
deleted theorem Nat.add_mul_div_right
deleted theorem Nat.add_mul_mod_self_left
deleted theorem Nat.add_one_ne_zero
deleted theorem Nat.div_eq_of_lt
deleted theorem Nat.div_eq_sub_div
deleted theorem Nat.div_lt_iff_lt_mul
deleted theorem Nat.div_mul_le_self
deleted theorem Nat.dvd_antisymm
deleted theorem Nat.dvd_iff_mod_eq_zero
deleted theorem Nat.dvd_mod_iff
deleted theorem Nat.dvd_of_mod_eq_zero
deleted theorem Nat.dvd_sub
deleted theorem Nat.eq_one_of_dvd_one
deleted theorem Nat.le_div_iff_mul_le
deleted theorem Nat.le_lt_antisymm
deleted theorem Nat.le_of_dvd
deleted theorem Nat.le_of_mod_lt
deleted theorem Nat.le_succ_of_pred_le
deleted theorem Nat.lt_le_antisymm
deleted theorem Nat.lt_succ_of_lt
deleted theorem Nat.min_succ_succ
deleted theorem Nat.mod_add_div
deleted theorem Nat.mod_add_mod
deleted theorem Nat.mod_eq_zero_of_dvd
deleted theorem Nat.mod_mod
deleted theorem Nat.mul_div_left
deleted theorem Nat.mul_div_right
deleted theorem Nat.mul_mod
deleted theorem Nat.mul_mod_left
deleted theorem Nat.mul_mod_mul_left
deleted theorem Nat.mul_mod_mul_right
deleted theorem Nat.mul_mod_right
deleted theorem Nat.mul_sub_div
deleted theorem Nat.one_add
deleted theorem Nat.one_pos
deleted theorem Nat.pos_of_dvd_of_pos
deleted theorem Nat.pow_eq
deleted theorem Nat.pow_succ'
deleted theorem Nat.pred_inj
deleted theorem Nat.pred_lt_pred
deleted theorem Nat.sub_eq_sub_min
deleted theorem Nat.sub_lt_succ
deleted theorem Nat.sub_mul_div
deleted theorem Nat.sub_mul_mod
deleted theorem Nat.sub_one_sub_lt
deleted theorem Nat.succ_add_eq_succ_add
deleted theorem Nat.succ_mul_succ_eq
deleted theorem Nat.succ_ne_self
deleted theorem Nat.succ_pred_eq_of_pos
deleted theorem Nat.succ_sub
deleted theorem Nat.succ_sub_one
deleted theorem Nat.succ_sub_sub_succ
deleted def Not.elim
deleted theorem Or.neg_resolve_left
deleted theorem Or.neg_resolve_right
deleted theorem Or.resolve_left
deleted theorem Or.resolve_right
deleted theorem not_congr
deleted theorem not_or_intro
deleted structure Lean.NameMapAttribute
deleted structure Lean.NameMapAttributeImpl
deleted theorem iff_of_false
deleted theorem iff_of_true
deleted def evalGuardHyp
deleted structure Mathlib.Tactic.Lint.Linter