Commit 2024-09-03 05:37 4810f3eb

View on Github →

chore: merge bump/v4.12.0 and move toolchain to v4.12.0-rc1 (#16433)

Estimated changes

modified theorem Subgroup.mk_eq_one
modified theorem LieSubmodule.coe_bracket
deleted theorem Bool.exists_bool'
deleted theorem Bool.exists_bool
deleted theorem Bool.forall_bool'
deleted theorem Bool.forall_bool
deleted theorem List.Sublist.of_cons_cons
deleted theorem List.append_left_eq_self
deleted theorem List.append_right_eq_self
deleted theorem List.drop_tail
deleted def List.foldlRecOn
deleted theorem List.foldlRecOn_nil
deleted def List.foldrRecOn
deleted theorem List.foldrRecOn_cons
deleted theorem List.foldrRecOn_nil
deleted theorem List.getElem?_eq
deleted theorem List.getElem_reverse
deleted theorem List.getLast?_cons_cons
deleted theorem List.isEmpty_iff_eq_nil
deleted theorem List.reverse_inj
deleted theorem List.self_eq_append_left
deleted theorem List.self_eq_append_right
deleted theorem List.tail_replicate
deleted theorem List.tail_sublist
deleted theorem List.take_cons
modified def Cycle.Mem
modified theorem List.mem_enum_iff_get?
deleted theorem List.findIdx_eq
deleted theorem List.findIdx_eq_length
deleted theorem List.findIdx_le_length
deleted theorem List.findIdx_lt_length
deleted theorem List.le_findIdx_of_not
deleted theorem List.lt_findIdx_of_not
deleted theorem List.not_of_lt_findIdx
deleted theorem List.IsPrefix.getElem
deleted theorem List.IsPrefix.head_eq
deleted theorem List.IsPrefix.ne_nil
deleted theorem List.dropLast_prefix
deleted theorem List.dropLast_sublist
deleted theorem List.dropLast_subset
deleted theorem List.dropWhile_suffix
deleted theorem List.infix_rfl
deleted theorem List.mem_of_mem_suffix
deleted theorem List.prefix_concat
deleted theorem List.prefix_concat_iff
deleted theorem List.prefix_iff_eq_append
deleted theorem List.prefix_iff_eq_take
deleted theorem List.prefix_rfl
deleted theorem List.prefix_take_iff
deleted theorem List.prefix_take_le_iff
deleted theorem List.suffix_iff_eq_append
deleted theorem List.suffix_iff_eq_drop
deleted theorem List.suffix_rfl
deleted theorem List.tail_suffix
deleted theorem List.takeWhile_prefix
deleted theorem List.bind_eq_nil
deleted theorem List.eq_iff_join_eq
deleted theorem List.join_eq_nil
deleted theorem List.join_filter_ne_nil
deleted theorem List.join_singleton
deleted theorem List.sublist_join
deleted theorem List.getElem_reverse'
deleted theorem List.Pairwise.pmap
deleted theorem List.pairwise_pmap
added theorem List.length_mergeSort'
deleted theorem List.length_mergeSort
added theorem List.map_mergeSort'
deleted theorem List.map_mergeSort
added theorem List.mem_mergeSort'
deleted theorem List.mem_mergeSort
added def List.mergeSort'
added theorem List.mergeSort'_nil
deleted def List.mergeSort
deleted theorem List.mergeSort_cons_cons
deleted theorem List.mergeSort_eq_self
deleted theorem List.mergeSort_nil
deleted theorem List.mergeSort_singleton
added theorem List.perm_mergeSort'
deleted theorem List.perm_mergeSort
added theorem List.sorted_mergeSort'
deleted theorem List.sorted_mergeSort
modified def Multiset.Mem
modified theorem Multiset.coe_sort
deleted theorem Nat.testBit_two_pow
deleted theorem Nat.testBit_two_pow_of_ne
deleted theorem Nat.testBit_two_pow_self
deleted theorem Option.get_map
deleted theorem Prod.«exists»
deleted theorem Prod.«forall»
deleted def Set.inclusion
modified theorem smooth_inclusion
modified theorem FreeGroup.Red.Step.sublist
modified theorem orderOf_eq_card_powers
deleted theorem exists₂_imp
deleted theorem Function.comp_const
deleted theorem Function.const_comp
deleted theorem nonempty_Prop
deleted theorem Relation.TransGen.trans
modified theorem Finpartition.mem_part
modified theorem PMF.map_comp
modified theorem Ideal.ofList_singleton
modified theorem IsClosed.HasSeparatingCover
deleted def timeCmdElab
modified def Edits
modified def calcNeeds
modified def getExplanations
modified theorem Lin_const