[Merged by Bors] - chore: classify removed @[ext] porting notes#11183

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

pitmonticone/removed-extleanprover-community/mathlib4:pitmonticone/removed-extCopy head branch name to clipboard