[Merged by Bors] - chore: classify new definition porting notes#11512

pitmonticone wants to merge 3 commits intomasterleanprover-community/mathlib4:masterfrom

pitmonticone/new-definitionleanprover-community/mathlib4:pitmonticone/new-definitionCopy head branch name to clipboard