[Merged by Bors] - chore: classify added lemma porting notes#10757

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

pitmonticone/added-lemmaleanprover-community/mathlib4:pitmonticone/added-lemmaCopy head branch name to clipboard