Commit 2024-07-30 00:15 d78ec33d

View on Github →

chore: replace zip_with -> zipWith in lemma names (#15218)

Estimated changes

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/List/Zip.lean

added theorem List.get?_zipWith'

added theorem List.get?_zipWith_eq_some

deleted theorem List.get?_zip_with

deleted theorem List.get?_zip_with_eq_some

added theorem List.getElem?_zipWith'

added theorem List.getElem?_zipWith_eq_some

deleted theorem List.getElem?_zip_with

deleted theorem List.getElem?_zip_with_eq_some