Commit 2024-03-05 04:47 fa48894a

View on Github →

chore: move Mathlib to v4.7.0-rc1 (#11162) This is a very large PR, but it has been reviewed piecemeal already in PRs to the bump/v4.7.0 branch as we update to intermediate nightlies.

Estimated changes

added def BitVec.adc'
added def BitVec.addLsb
added def BitVec.getLsb'
added def BitVec.getMsb'
added def BitVec.sbb
added def BitVec.toBEList
added def BitVec.toLEList
deleted def Std.BitVec.adc'
deleted def Std.BitVec.addLsb
deleted def Std.BitVec.getLsb'
deleted def Std.BitVec.getMsb'
deleted def Std.BitVec.sbb
deleted def Std.BitVec.toBEList
deleted def Std.BitVec.toLEList
added theorem BitVec.addLsb_div_two
added theorem BitVec.extractLsb_eq
added theorem BitVec.ofFin_and
added theorem BitVec.ofFin_mul
added theorem BitVec.ofFin_natCast
added theorem BitVec.ofFin_neg
added theorem BitVec.ofFin_nsmul
added theorem BitVec.ofFin_ofNat
added theorem BitVec.ofFin_one
added theorem BitVec.ofFin_or
added theorem BitVec.ofFin_pow
added theorem BitVec.ofFin_toFin
added theorem BitVec.ofFin_val
added theorem BitVec.ofFin_xor
added theorem BitVec.ofFin_zero
added theorem BitVec.ofFin_zsmul
added theorem BitVec.ofNat_toNat'
added theorem BitVec.toFin_inj
added theorem BitVec.toFin_injective
added theorem BitVec.toFin_natCast
added theorem BitVec.toFin_neg
added theorem BitVec.toFin_nsmul
added theorem BitVec.toFin_ofFin
added theorem BitVec.toFin_one
added theorem BitVec.toFin_pow
added theorem BitVec.toFin_val
added theorem BitVec.toFin_zero
added theorem BitVec.toFin_zsmul
added theorem BitVec.toNat_inj
added theorem BitVec.toNat_injective
added theorem BitVec.toNat_lt_toNat
deleted theorem Std.BitVec.addLsb_div_two
deleted theorem Std.BitVec.extractLsb_eq
deleted theorem Std.BitVec.ofFin_and
deleted theorem Std.BitVec.ofFin_mul
deleted theorem Std.BitVec.ofFin_natCast
deleted theorem Std.BitVec.ofFin_neg
deleted theorem Std.BitVec.ofFin_nsmul
deleted theorem Std.BitVec.ofFin_ofNat
deleted theorem Std.BitVec.ofFin_one
deleted theorem Std.BitVec.ofFin_or
deleted theorem Std.BitVec.ofFin_pow
deleted theorem Std.BitVec.ofFin_toFin
deleted theorem Std.BitVec.ofFin_val
deleted theorem Std.BitVec.ofFin_xor
deleted theorem Std.BitVec.ofFin_zero
deleted theorem Std.BitVec.ofFin_zsmul
deleted theorem Std.BitVec.ofNat_toNat'
deleted theorem Std.BitVec.toFin_inj
deleted theorem Std.BitVec.toFin_natCast
deleted theorem Std.BitVec.toFin_neg
deleted theorem Std.BitVec.toFin_nsmul
deleted theorem Std.BitVec.toFin_ofFin
deleted theorem Std.BitVec.toFin_one
deleted theorem Std.BitVec.toFin_pow
deleted theorem Std.BitVec.toFin_val
deleted theorem Std.BitVec.toFin_zero
deleted theorem Std.BitVec.toFin_zsmul
deleted theorem Std.BitVec.toNat_inj
deleted theorem Std.BitVec.toNat_lt_toNat
modified theorem Bool.not_false'
modified def Fin2.elim0
deleted theorem Nat.mod_mul_left_mod
deleted theorem Nat.mod_mul_right_mod
deleted theorem Nat.mod_mul_left_div_self
deleted theorem Nat.mod_pow_succ
modified theorem Nat.two_pow_succ
modified theorem UFModel.Agrees.empty
modified theorem Set.nil_mem_subchain
deleted def Tests.eq2
deleted theorem Tests.eq2_symm
added structure A