Commit 2026-09-17 16:25 6c8ecb8f
View on Github →doc: add library note about scoping simp lemmas with weak keys (#39449)
In PR #39262 I noticed that some simp lemmas were scoped for a reason that is not immediately obvious, so I figured that adding a library note would be nice in case anyone else runs into this in the future (this pattern is quite common in Mathlib!)
In case it's helpful for review, here are links to a few of the PRs that added this scoping initially: