Commit 2022-12-14 23:02 e8fa7b2c

View on Github →

fix: initialize simps for FunLike structures (#1014) Because coercions and bundling has changed, we have to give all simps projections of all FunLike structures manually for now (#1013). Fixes linting issues in #977

Estimated changes

Modified Mathlib/Algebra/Hom/Group.lean

added def MonoidHom.Simps.apply

added def MonoidWithZeroHom.Simps.apply

added def MulHom.Simps.apply

added def OneHom.Simps.apply

Modified Mathlib/Algebra/Hom/Ring.lean

added def NonUnitalRingHom.Simps.apply

added def RingHom.Simps.apply

Modified Mathlib/Order/Hom/Basic.lean

added def OrderHom.Simps.coe

Modified Mathlib/Order/RelIso/Basic.lean

added def RelHom.Simps.apply