[Merged by Bors] - chore: classify removed @[pp_nodot] porting notes#11181

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

pitmonticone/removed-pp_nodotleanprover-community/mathlib4:pitmonticone/removed-pp_nodotCopy head branch name to clipboard