mathlib3
16552e6a - fix(group_theory/submonoid): looping simp lemma (#2447)

Commit
5 years ago
fix(group_theory/submonoid): looping simp lemma (#2447) Removes a `@[nolint simp_nf]`. I have no idea why I didn't notice this earlier, but `coe_coe` loops due to `coe_sort_coe_base` since `submonoid` doesn't have it's own `has_coe_to_sort` instance.
Author
Parents
Loading