[Merged by Bors] - chore: classify "added theorem" porting notes#11513

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

pitmonticone/added-theoremleanprover-community/mathlib4:pitmonticone/added-theoremCopy head branch name to clipboard