Commit 2023-08-08 09:48 5f5bef5a

View on Github →

chore: bump Std version (#6435) Notably there is now a l1 ∪ l2 notation for List.union.

Estimated changes

Modified Mathlib/Data/List/Card.lean

modified theorem List.union_equiv_append

Modified Mathlib/Data/List/Intervals.lean

Modified Mathlib/Data/List/Lattice.lean

deleted theorem List.mem_inter

deleted theorem List.mem_union

Modified Mathlib/Data/List/Perm.lean

modified theorem List.Perm.union_left

Modified Mathlib/Data/Multiset/FinsetOps.lean

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/Data/Nat/PrimeFin.lean

Modified Mathlib/Data/String/Basic.lean

deleted theorem String.Iterator.hasNext_cons_addChar

Modified lake-manifest.json