Commit 2024-07-31 18:23 0a717792

View on Github →

chore: remove obsolete comments about @[congr] (#15299) Some of these have been commented out since this file was added to mathlib 3, others refer to theorems that have been upstreamed. In any case, they are not actionable.

Estimated changes