Commit 2024-05-02 13:42 db651742

View on Github →

chore: move to v4.8.0-rc1 (#12548) This moves Mathlib to v4.8.0-rc1

Estimated changes

modified def Cache.Hashing.roots
modified theorem Nat.cast_add_one_ne_zero
modified theorem Composition.index_exists
deleted theorem Bool.beq_comm
deleted theorem Bool.beq_eq_decide_eq
deleted theorem Bool.coe_iff_coe
deleted theorem Bool.cond_decide
deleted theorem Bool.cond_eq_ite
deleted theorem Bool.cond_not
deleted theorem Bool.decide_and
deleted theorem Bool.decide_coe
deleted theorem Bool.decide_or
deleted theorem Bool.default_bool
deleted theorem Bool.not_eq_not
deleted theorem Bool.not_not_eq
deleted theorem List.getD_cons_succ
deleted theorem List.getD_cons_zero
deleted theorem List.getD_nil
modified theorem Nat.one_lt_succ_succ
deleted theorem Nat.pred_eq_sub_one
modified theorem Nat.pred_eq_succ_iff
modified theorem Nat.rec_add_one
added theorem Nat.rec_one
deleted theorem Nat.dist.def
modified theorem Rat.num_nonneg
modified def UInt8.toChar
deleted theorem UInt8.toChar_aux
modified theorem Vector3.append_insert
modified def Vector3.cons
modified def Vector3.consElim
modified theorem Vector3.cons_head_tail
modified def Vector3.head
modified def Vector3.insert
modified theorem Vector3.insert_fs
modified def Vector3.tail
deleted theorem Bool.cond_false
deleted theorem Bool.cond_self.{u}
deleted theorem Bool.cond_true
deleted theorem Bool.ite_eq_false_distrib
deleted theorem Bool.ite_eq_true_distrib
deleted theorem Ne.def
deleted def Lean.Expr.foldlM
deleted def Lean.MVarId.iffOfEq
deleted def Lean.MVarId.propext
modified theorem and_or_imp
deleted theorem eq_true_eq_id
deleted theorem if_false_left
deleted theorem if_false_right
deleted theorem if_true_left
deleted theorem if_true_right
modified theorem imp_and_neg_imp_iff
modified theorem imp_iff_right_iff
modified theorem harmonic_eq_sum_Icc
modified theorem Ordinal.succ_one
deleted def Foo.Foo.foo
deleted def add.add
added theorem foo
deleted theorem prime_of_prime
added def testConst
deleted def zero