Commit 2023-11-21 12:27 366aa49a

View on Github →

chore: bump std4 (#8548)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.length_dropLast

Modified Mathlib/Data/Prod/Basic.lean

deleted theorem Prod.ext

Modified Mathlib/Data/Sigma/Basic.lean

deleted theorem PSigma.ext

deleted theorem Sigma.ext

Modified Mathlib/Logic/Basic.lean

Modified lake-manifest.json