Commit 2024-07-01 02:54 f5c3f06a

View on Github →

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

Estimated changes

modified theorem Imo1994Q1.tedious
modified theorem Fin.prod_univ_get
modified theorem PiLp.dist_eq_iSup
modified theorem PiLp.edist_eq_iSup
modified theorem PiLp.norm_eq_ciSup
modified theorem WithLp.prod_norm_eq_sup
modified theorem lp.norm_eq_ciSup
modified theorem Composition.blocks_pos'
modified theorem Composition.one_le_blocks'
modified theorem YoungDiagram.get_rowLens
added theorem Fin.neg_def
modified theorem Finset.card_eq_zero
modified theorem Fin.univ_image_get'
deleted theorem List.eq_nil_of_map_eq_nil
deleted theorem List.foldl_map'
deleted theorem List.foldr_map'
added theorem List.getElem?_indexOf
added theorem List.getElem?_length
added theorem List.getElem?_pmap
added theorem List.getElem_attach
added theorem List.getElem_indexOf
added theorem List.getElem_map_rev
added theorem List.getElem_pmap
added theorem List.getElem_reverse
added theorem List.getElem_set_of_ne
added theorem List.getLast?_eq_none
deleted theorem List.getLast?_isNone
deleted theorem List.getLast_map
modified theorem List.get_reverse
modified theorem List.get_reverse_aux₂
deleted theorem List.head?_map
modified theorem List.indexOf_get
deleted theorem List.join_replicate_nil
deleted theorem List.map_bind
deleted theorem List.map_concat
deleted theorem List.map_congr
deleted theorem List.map_const'
deleted theorem List.map_const
deleted theorem List.map_eq_foldr
deleted theorem List.map_eq_map_iff
deleted theorem List.map_eq_replicate_iff
deleted theorem List.map_filter_eq_foldr
deleted theorem List.map_id''
deleted theorem List.map_join
deleted theorem List.map_replicate
deleted theorem List.map_reverse
modified theorem List.replicate_left_inj
deleted theorem List.replicate_one
modified theorem List.replicate_right_inj'
deleted theorem List.replicate_zero
deleted theorem List.reverse_replicate
deleted theorem List.takeWhile_cons
deleted theorem List.takeWhile_nil
deleted theorem List.enum_cons
deleted theorem List.enum_nil
modified theorem List.get?_enumFrom
added theorem List.getElem?_enum
added theorem List.getElem?_enumFrom
added theorem List.getElem_enum
added theorem List.getElem_enumFrom
modified theorem List.getD_map
added theorem List.IsPrefix.getElem
added theorem List.getElem_inits
added theorem List.getElem_tails
deleted theorem List.insert_nil
modified theorem List.get?_iterate
added theorem List.getElem?_iterate
added theorem List.getElem_iterate
modified theorem List.Nodup.erase_get
added theorem List.indexOf_getElem
modified theorem List.get?_ofFn
added theorem List.getElem?_ofFn
added theorem List.getElem_ofFn
added theorem List.getElem_ofFn_go
added theorem List.ofFn_getElem
added theorem List.getElem_finRange
added theorem List.getElem?_rotate
added theorem List.getElem_rotate
modified theorem List.head?_rotate
added theorem List.getElem?_zip_with
added theorem List.getElem_zip
added theorem List.getElem_zipWith
added theorem Multiset.filter_map
deleted theorem Multiset.map_filter
deleted theorem Nat.add_one_le_iff
deleted theorem Nat.lt_add_one_iff
added theorem Part.toOption_eq_none
deleted theorem Part.toOption_isNone
added theorem Prod.map_apply'
deleted theorem Prod.map_apply
deleted theorem Prod.map_fst
deleted theorem Prod.map_snd
modified theorem Set.range_list_getD
modified theorem Set.range_list_getI
deleted theorem List.bind_assoc
deleted theorem List.bind_singleton'
deleted theorem List.bind_singleton
deleted theorem List.map_eq_bind
deleted theorem Nat.add_one_pos
modified theorem Cardinal.lift_iInf
modified theorem Cardinal.lift_max
modified theorem Cardinal.lift_min
modified theorem Cardinal.lift_sInf
modified theorem Cardinal.lift_succ