[Merged by Bors] - chore(Algebra/Ring/CharZero): document scoped simp design choice#39262

Paul-Lez wants to merge 3 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Paul-Lez:remove-scoped-simpsPaul-Lez/mathlib4:remove-scoped-simpsCopy head branch name to clipboard