Commit 2024-10-17 07:12 9caf5284

View on Github →

chore: cleanup in Data/Prod/Basic (#17841)

Estimated changes

Modified Mathlib/Data/List/NatAntidiagonal.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Multiset/Antidiagonal.lean

Modified Mathlib/Data/Prod/Basic.lean

deleted theorem Prod.map_mk