Commit 2025-05-02 23:00 01239f49

View on Github →

chore: bump toolchain to v4.20.0-rc2 (#24561)

Estimated changes

deleted def SheafOfModules.unit
deleted def Subbimodule.mk
deleted def CStarMatrix.toCLM
deleted def convexAddSubmonoid
modified theorem BitVec.toFin_pow
deleted theorem Int.add_emod_left
deleted theorem Int.add_emod_right
deleted theorem Int.natCast_emod
deleted theorem Int.sub_emod_right
deleted theorem Int.coe_lcm_dvd
deleted theorem Int.dvd_coe_gcd
deleted theorem Int.gcd_assoc
deleted theorem Int.gcd_comm
deleted theorem Int.gcd_div
deleted theorem Int.gcd_div_gcd_div_gcd
deleted theorem Int.gcd_dvd_gcd_mul_left
deleted theorem Int.gcd_dvd_gcd_mul_right
deleted theorem Int.gcd_eq_left
deleted theorem Int.gcd_eq_right
deleted theorem Int.gcd_eq_zero_iff
deleted theorem Int.gcd_mul_lcm
deleted theorem Int.gcd_mul_left
deleted theorem Int.gcd_mul_right
deleted theorem Int.gcd_pos_iff
deleted theorem Int.gcd_self
deleted theorem Int.gcd_zero_left
deleted theorem Int.gcd_zero_right
deleted theorem Int.lcm_assoc
deleted theorem Int.lcm_comm
deleted theorem Int.lcm_mul_left
deleted theorem Int.lcm_mul_right
deleted theorem Int.lcm_one_left
deleted theorem Int.lcm_one_right
deleted theorem Int.lcm_zero_left
deleted theorem Int.lcm_zero_right
deleted theorem Int.pow_dvd_pow_iff
deleted theorem Int.cast_id
modified theorem Int.div_dvd_iff_dvd_mul
modified theorem Int.dvd_div_of_mul_dvd
modified theorem Int.dvd_mul_of_div_dvd
deleted theorem Int.ediv_dvd_ediv
deleted theorem Int.ediv_dvd_of_dvd
modified theorem Int.emod_two_eq_zero_or_one
deleted theorem Int.le_add_one_iff
deleted theorem Int.le_sub_one_iff
deleted theorem Int.lt_of_toNat_lt
deleted theorem Int.lt_toNat
deleted theorem Int.natAbs_add_of_nonneg
deleted theorem Int.natAbs_add_of_nonpos
deleted theorem Int.natAbs_cast
deleted theorem Int.natAbs_ediv_of_dvd
deleted theorem Int.natAbs_eq_of_dvd_dvd
deleted theorem Int.natAbs_ofNat'
deleted theorem Int.natAbs_pow
deleted theorem Int.natAbs_sq
deleted theorem Int.natCast_ediv
deleted theorem Int.natCast_eq_zero
deleted theorem Int.natCast_inj
modified theorem Int.natCast_mod
deleted theorem Int.natCast_ne_zero
deleted theorem Int.natCast_nonneg
deleted theorem Int.natCast_nonpos_iff
deleted theorem Int.natCast_pos
deleted theorem Int.natCast_succ_pos
deleted theorem Int.neg_emod_two
deleted theorem Int.ofNat_eq_natCast
modified theorem Int.sign_mul_self_eq_natAbs
deleted theorem Int.sign_natCast_add_one
deleted theorem Int.sub_one_lt_iff
modified theorem Int.toNat_lt''
deleted theorem Int.toNat_natCast
deleted theorem Int.toNat_natCast_add_one
deleted theorem Int.toNat_sub_of_le
deleted theorem List.getLast_cons_cons
deleted theorem Nat.pow_eq_self_iff
deleted theorem Nat.lcm_dvd_iff
deleted theorem Nat.lcm_dvd_mul
deleted theorem Nat.lcm_mul_left
deleted theorem Nat.lcm_mul_right
deleted theorem Nat.lcm_pos
deleted theorem Nat.add_eq_max_iff
deleted theorem Nat.add_eq_min_iff
deleted theorem Nat.add_eq_one_iff
deleted theorem Nat.add_eq_three_iff
deleted theorem Nat.add_eq_two_iff
deleted theorem Nat.add_mod_eq_ite
deleted theorem Nat.add_sub_one_le_mul
deleted theorem Nat.add_succ_lt_add
deleted theorem Nat.add_succ_sub_one
deleted theorem Nat.default_eq_zero
deleted theorem Nat.div_add_mod'
deleted theorem Nat.div_div_div_eq_div
deleted theorem Nat.div_dvd_iff_dvd_mul
deleted theorem Nat.div_dvd_of_dvd
deleted theorem Nat.div_eq_self
deleted theorem Nat.div_eq_sub_mod_div
deleted theorem Nat.div_lt_one_iff
deleted theorem Nat.div_mul_div_comm
deleted theorem Nat.div_mul_div_le_div
deleted theorem Nat.dvd_div_iff_mul_dvd
deleted theorem Nat.dvd_div_of_mul_dvd
deleted theorem Nat.dvd_iff_div_mul_eq
deleted theorem Nat.dvd_iff_dvd_dvd
deleted theorem Nat.dvd_iff_le_div_mul
deleted theorem Nat.dvd_mul_of_div_dvd
deleted theorem Nat.dvd_sub_mod
modified theorem Nat.eq_zero_of_double_le
deleted theorem Nat.eq_zero_of_dvd_of_lt
deleted theorem Nat.eq_zero_of_le_div
modified theorem Nat.eq_zero_of_le_half
deleted theorem Nat.eq_zero_of_mul_le
modified theorem Nat.half_le_of_sub_le_half
deleted theorem Nat.le_add_one_iff
deleted theorem Nat.le_add_pred_of_pos
deleted theorem Nat.le_and_le_add_one_iff
modified theorem Nat.le_half_of_half_lt_sub
deleted theorem Nat.le_iff_ne_zero_of_dvd
deleted theorem Nat.le_mul_self
deleted theorem Nat.le_of_lt_add_of_dvd
deleted theorem Nat.le_of_pred_lt
deleted theorem Nat.le_self_pow
deleted theorem Nat.le_succ_iff
deleted theorem Nat.lt_div_mul_add
deleted theorem Nat.lt_iff_add_one_le
deleted theorem Nat.lt_iff_le_pred
deleted theorem Nat.lt_mul_div_succ
deleted theorem Nat.lt_mul_of_div_lt
deleted theorem Nat.lt_mul_self_iff
deleted theorem Nat.lt_of_div_lt_div
deleted theorem Nat.lt_of_lt_pred
deleted theorem Nat.lt_of_pow_dvd_right
deleted theorem Nat.lt_one_add_iff
deleted theorem Nat.lt_pred_iff
deleted theorem Nat.max_eq_zero_iff
deleted theorem Nat.min_eq_zero_iff
deleted theorem Nat.mod_add_div'
deleted theorem Nat.mod_eq_iff_lt
deleted theorem Nat.mod_succ
deleted theorem Nat.mod_succ_eq_iff_lt
deleted theorem Nat.mod_two_ne_one
deleted theorem Nat.mod_two_ne_zero
deleted theorem Nat.mod_two_not_eq_one
deleted theorem Nat.mod_two_not_eq_zero
deleted theorem Nat.mul_add_mod'
deleted theorem Nat.mul_add_mod_of_lt
modified theorem Nat.mul_def
deleted theorem Nat.mul_div_eq_iff_dvd
deleted theorem Nat.mul_dvd_of_dvd_div
deleted theorem Nat.mul_eq_left
deleted theorem Nat.mul_eq_right
deleted theorem Nat.mul_lt_mul''
deleted theorem Nat.mul_lt_mul_pow_succ
deleted theorem Nat.mul_self_inj
deleted theorem Nat.mul_self_le_mul_self
deleted theorem Nat.mul_self_lt_mul_self
deleted theorem Nat.mul_sub_div_of_dvd
deleted theorem Nat.not_dvd_of_pos_of_lt
modified theorem Nat.not_pos_pow_dvd
deleted theorem Nat.not_succ_lt_self
deleted theorem Nat.one_add_le_iff
deleted theorem Nat.one_le_div_iff
deleted theorem Nat.one_le_iff_ne_zero
deleted theorem Nat.one_le_of_lt
deleted theorem Nat.one_le_pow
deleted theorem Nat.one_lt_mul_iff
deleted theorem Nat.one_lt_pow'
deleted theorem Nat.one_lt_pow
deleted theorem Nat.one_lt_pow_iff
deleted theorem Nat.one_lt_succ_succ
deleted theorem Nat.one_lt_two_pow'
deleted theorem Nat.one_mod
deleted theorem Nat.one_mod_eq_one
deleted theorem Nat.pow_mod
deleted theorem Nat.pow_self_pos
deleted theorem Nat.pred_add_self
deleted theorem Nat.pred_eq_of_eq_succ
deleted theorem Nat.pred_eq_self_iff
deleted theorem Nat.pred_eq_succ_iff
deleted theorem Nat.pred_le_iff
deleted theorem Nat.pred_one_add
deleted theorem Nat.pred_sub
deleted theorem Nat.self_add_pred
deleted theorem Nat.self_add_sub_one
deleted theorem Nat.sq_sub_sq
deleted theorem Nat.sub_mul_div'
deleted theorem Nat.sub_one_add_self
deleted theorem Nat.sub_succ'
deleted theorem Nat.succ_add_sub_one
deleted theorem Nat.succ_le_iff
deleted theorem Nat.succ_mul_pos
deleted theorem Nat.succ_ne_succ
deleted theorem Nat.succ_succ_ne_one
deleted theorem Nat.two_pow_succ
deleted theorem Option.bnot_comp_isNone
deleted theorem Option.bnot_comp_isSome
deleted theorem Option.bnot_isNone
deleted theorem Option.bnot_isSome
deleted theorem Option.eq_none_or_eq_some
deleted theorem Option.exists_ne_none
deleted theorem Option.liftOrGet_choice
modified theorem Option.none_bind'
deleted theorem Option.none_orElse'
deleted theorem Option.orElse_eq_none'
modified theorem Option.orElse_eq_none
deleted theorem Option.orElse_eq_some'
deleted theorem Option.orElse_none'
deleted theorem Option.pbind_eq_bind
deleted theorem Option.pbind_eq_some
deleted theorem Option.pbind_map
modified theorem Option.some_bind'
deleted theorem Option.some_orElse'
deleted theorem Option.mem_some_iff
deleted def Hyperreal.ofReal
deleted def Hyperreal.ofSeq
deleted theorem $typeName.intCast_def
deleted theorem $typeName.natCast_def
deleted theorem $typeName.neg_def
deleted theorem $typeName.nsmul_def
deleted theorem $typeName.pow_def
deleted theorem $typeName.toFin_injective
deleted theorem $typeName.val_injective
deleted theorem $typeName.zsmul_def
deleted def toLinearExtension
deleted def differentIdeal
deleted def Ideal.relNorm
deleted def Ideal.spanNorm
deleted structure Lean.Expr.LiftLetsConfig
deleted def Lean.Expr.liftLets
deleted def a