Commit 2022-04-14 06:30 2249a240
View on Github →chore(*): suggestions from the generalisation linter (#13092)
Prompted by zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/An.20example.20of.20why.20formalization.20is.20useful
These are the "reasonable" suggestions from @alexjbest's generalisation linter up to algebra.group.basic.