Zulip Chat Archive

Stream: PR reviews

Topic: PR 33276 Review

Nicola Bernini (Dec 26 2025 at 16:28):

Hi,
I have recently submitted the simple PR
https://github.com/leanprover-community/mathlib4/pull/33276
and it's ready for review, it passed all the automated checks

Weiyi Wang (Dec 26 2025 at 16:30):

tip: use "#33276" and zulip will make it a link to the PR. Also putting the PR title here can help finding people with related knowledge

Weiyi Wang (Dec 26 2025 at 16:32):

What's the motivation behind the renaming?

Aaron Liu (Dec 26 2025 at 16:51):

conflict with reverse_perm'

Nicola Bernini (Dec 26 2025 at 18:24):

Shall I rename reverse_perm'​ to reverse_perm_iff​or any other suggestion?
Lmk so I can finalize the PR

Last updated: Feb 28 2026 at 14:05 UTC