Commit 2025-09-24 16:53 44aa061c

View on Github →

fix: adaptations for batteries#1421 (#29928) Fixes the mathlib build after leanprover-community/batteries#1421.

Estimated changes

deleted theorem List.Chain.count_not
deleted theorem List.Chain'.append
deleted theorem List.Chain'.chain
deleted theorem List.Chain'.cons'
deleted theorem List.Chain'.cons_cons
deleted theorem List.Chain'.cons_of_le
deleted theorem List.Chain'.drop
deleted theorem List.Chain'.iff
deleted theorem List.Chain'.iff_mem
deleted theorem List.Chain'.imp
deleted theorem List.Chain'.imp_head
deleted theorem List.Chain'.induction
deleted theorem List.Chain'.infix
deleted theorem List.Chain'.init
deleted theorem List.Chain'.prefix
deleted theorem List.Chain'.rel_head
deleted theorem List.Chain'.rel_head?
deleted theorem List.Chain'.suffix
deleted theorem List.Chain'.tail
deleted theorem List.Chain'.take
deleted theorem List.Chain.iff
deleted theorem List.Chain.iff_mem
deleted theorem List.Chain.induction
added theorem List.IsChain.append
added theorem List.IsChain.cons'
added theorem List.IsChain.drop
added theorem List.IsChain.dropLast
added theorem List.IsChain.iff
added theorem List.IsChain.iff_mem
added theorem List.IsChain.imp_head
added theorem List.IsChain.induction
added theorem List.IsChain.infix
added theorem List.IsChain.prefix
added theorem List.IsChain.rel_head
added theorem List.IsChain.rel_head?
added theorem List.IsChain.suffix
added theorem List.IsChain.tail
added theorem List.IsChain.take
deleted theorem List.Pairwise.chain'
deleted theorem List.chain'_append
deleted theorem List.chain'_attach
deleted theorem List.chain'_attachWith
deleted theorem List.chain'_cons'
deleted theorem List.chain'_cons_cons
deleted theorem List.chain'_flatten
deleted theorem List.chain'_iff_get
deleted theorem List.chain'_iff_pairwise
deleted theorem List.chain'_isInfix
deleted theorem List.chain'_map
deleted theorem List.chain'_map_of_chain'
deleted theorem List.chain'_nil
deleted theorem List.chain'_of_chain'_map
deleted theorem List.chain'_of_not
deleted theorem List.chain'_pair
deleted theorem List.chain'_reverse
deleted theorem List.chain'_singleton
deleted theorem List.chain'_split
deleted theorem List.chain_iff_forall₂
deleted theorem List.chain_iff_get
deleted theorem List.chain_iff_pairwise
deleted theorem List.chain_map
deleted theorem List.chain_map_of_chain
deleted theorem List.chain_of_chain_map
deleted theorem List.chain_of_chain_pmap
deleted theorem List.chain_pmap_of_chain
deleted theorem List.chain_singleton
deleted theorem List.chain_split
added theorem List.isChain_append
added theorem List.isChain_attach
added theorem List.isChain_cons'
added theorem List.isChain_cons_iff
added theorem List.isChain_cons_map
added theorem List.isChain_cons_pmap
added theorem List.isChain_flatten
added theorem List.isChain_iff_get
added theorem List.isChain_isInfix
added theorem List.isChain_map
added theorem List.isChain_nil
added theorem List.isChain_pair
added theorem List.isChain_pmap
added theorem List.isChain_reverse
added theorem List.isChain_singleton
added theorem List.isChain_split
deleted theorem List.chain'_ofFn
added theorem List.isChain_ofFn
added theorem Cycle.chain_range_succ
modified theorem List.destutter'_eq_self_iff
deleted theorem List.destutter'_is_chain'
deleted theorem List.destutter'_is_chain
deleted theorem List.destutter'_of_chain
modified theorem List.destutter_eq_self_iff
deleted theorem List.destutter_is_chain'
deleted theorem List.destutter_of_chain'
added theorem List.isChain_destutter
deleted theorem List.Ico.chain'_succ
added theorem List.Ico.isChain_succ
deleted theorem List.chain'_range_succ
deleted theorem List.chain_range_succ
added theorem List.isChain_range
modified theorem List.tfae_of_cycle
modified def List.IsZeckendorfRep
modified theorem FreeGroup.IsReduced.infix
modified theorem FreeGroup.IsReduced.nil
modified def FreeGroup.IsReduced
deleted theorem Denumerable.raise'_chain
modified theorem Denumerable.raise'_sorted
deleted theorem Denumerable.raise_chain
modified theorem Denumerable.raise_sorted
modified theorem Set.nil_mem_subchain
deleted theorem RelSeries.toList_chain'