[Merged by Bors] - chore: classify broken dot notation porting notes#11038

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

pitmonticone/broken-dot-notationleanprover-community/mathlib4:pitmonticone/broken-dot-notationCopy head branch name to clipboard