[Merged by Bors] - chore: classify rw to erw porting notes#11225

pitmonticone wants to merge 1 commit intomasterleanprover-community/mathlib4:masterfrom

pitmonticone/rw-to-erwleanprover-community/mathlib4:pitmonticone/rw-to-erwCopy head branch name to clipboard