Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 00:49 06fdc087

View on Github →

chore(algebra/group/pi): replace a lemma with @[simps] (#6203)

Estimated changes

Modified src/algebra/group/pi.lean

modified def add_monoid_hom.single

deleted theorem add_monoid_hom.single_apply