Commit 2020-03-30 20:13 8a617238

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