Commit 2020-06-22 18:22 f0593365

fix(algebra/pi_instances): improve definitions of pi.* (#3116) The new test/pi_simp.lean fails with current master. Note that this is a workaround, not a proper fix for tactic.pi_instance. See also Zulip chat Also use @[to_additive] to generate additive definitions, add ordered multiplicative monoids, and add semimodule (Π i, f i) (Π, g i).