feat: Rename List.reverse_perm to List.reverse_perm_self and List.reverse_perm' to List.reverse_perm_iff#33276
Conversation
PR summary a36c84ab82Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
I'm afraid this isn't what was intended - or at least only part of it. The renaming would need to be done in the lean4 repository first.
However, I'm not convinced that would be a good change anyway. Instead, I suggest two renames below that I think make more sense. Tagging @Paul-Lez who added the TODO in #22977.
If you make this change, please make sure to update the PR title.
Mathlib/Data/List/Basic.lean
Outdated
| simp only [reverseAux_eq, map_append, map_reverse] | ||
|
|
||
| -- TODO: Rename `List.reverse_perm` to `List.reverse_perm_self` | ||
| @[simp] lemma reverse_perm' : l₁.reverse ~ l₂ ↔ l₁ ~ l₂ where |
There was a problem hiding this comment.
This to reverse_perm_iff
| mp := l₁.reverse_perm_self.symm.trans | ||
| mpr := l₁.reverse_perm_self.trans | ||
|
|
||
| @[simp] lemma perm_reverse : l₁ ~ l₂.reverse ↔ l₁ ~ l₂ where |
There was a problem hiding this comment.
And this to perm_reverse_iff
|
And most importantly: thanks for the contribution! |
…b.com:NicolaBernini/mathlib4 into feat/reverse-perm-to-reverse-perm-self-rename
|
This pull request has conflicts, please merge |
Uh oh!
There was an error while loading. Please reload this page.