Commit 2023-06-01 13:37 01da6a3c

View on Github →

chore: bump to nightly-2023-05-31 (#4530)

Estimated changes

Modified Mathlib/Algebra/EuclideanDomain/Defs.lean

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

Modified Mathlib/Analysis/NormedSpace/LpSpace.lean

Modified Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

Modified Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

Modified Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean

Modified Mathlib/CategoryTheory/Sites/InducedTopology.lean

Modified Mathlib/Control/LawfulFix.lean

Modified Mathlib/Data/Dfinsupp/Basic.lean

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/Data/List/Basic.lean

deleted def List.attach

deleted def List.pmap

Modified Mathlib/Data/List/Chain.lean

deleted theorem List.Chain.imp'

deleted theorem List.Chain.imp

deleted theorem List.chain_of_chain_cons

deleted theorem List.rel_of_chain_cons

Modified Mathlib/Data/List/Defs.lean

deleted theorem List.chain_cons

Modified Mathlib/Data/List/Intervals.lean

Modified Mathlib/Data/List/Range.lean

deleted theorem List.chain_lt_range'

deleted theorem List.chain_succ_range'

added theorem List.enumFrom_eq_zip_range'

deleted theorem List.enum_from_eq_zip_range'

deleted theorem List.enum_from_map_fst

deleted theorem List.enum_map_fst

deleted theorem List.get?_range'

deleted theorem List.get?_range

deleted theorem List.get_range'

deleted theorem List.get_range

deleted theorem List.iota_eq_reverse_range'

deleted theorem List.length_iota

deleted theorem List.length_range'

deleted theorem List.length_range

deleted theorem List.map_add_range'

deleted theorem List.map_sub_range'

deleted theorem List.mem_iota

deleted theorem List.mem_range'

deleted theorem List.mem_range

modified theorem List.nodup_range'

deleted theorem List.not_mem_range_self

modified theorem List.nthLe_range'

added theorem List.nthLe_range'_1

modified theorem List.pairwise_lt_range'

deleted theorem List.range'_append

deleted theorem List.range'_concat

deleted theorem List.range'_eq_map_range

deleted theorem List.range'_eq_nil

added theorem List.range'_one

deleted theorem List.range'_sublist_right

deleted theorem List.range'_subset_right

deleted theorem List.range_add

deleted theorem List.range_eq_nil

deleted theorem List.range_eq_range'

deleted theorem List.range_loop_range'

deleted theorem List.range_sublist

deleted theorem List.range_subset

deleted theorem List.range_succ

deleted theorem List.range_succ_eq_map

deleted theorem List.range_zero

deleted theorem List.reverse_range'

deleted theorem List.self_mem_range_succ

added theorem List.unzip_enumFrom_eq_prod

deleted theorem List.unzip_enum_from_eq_prod

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

Modified Mathlib/Data/Polynomial/Identities.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

Modified Mathlib/LinearAlgebra/BilinearForm.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem exists_comm

Modified Mathlib/Logic/Equiv/List.lean

Modified Mathlib/ModelTheory/LanguageMap.lean

Modified Mathlib/Order/LocallyFinite.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Monad.lean

Modified Mathlib/RingTheory/IntegralClosure.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

Modified Mathlib/Topology/Sheaves/PresheafOfFunctions.lean

Modified lake-manifest.json

Modified lean-toolchain