mathlib3
fix(algebra/punit_instance): punit.smul_eq is marked simp and can be proved by simp
#2291

Merged

fix(algebra/punit_instance): punit.smul_eq is marked simp and can be proved by simp #2291

mergify merged 1 commit into master from ChrisHughes24-patch-1

fix(algebra/punit_instance): punit.smul_eq is marked simp and can be …

4b8acd3c

gebner approved these changes on 2020-03-30

gebner added ready-to-merge

mergify merged 8a617238 into master 5 years ago

robertylewis deleted the ChrisHughes24-patch-1 branch 5 years ago

Reviewers

gebner

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone