Commit 2025-01-29 00:09 de761503
View on Github →feat(Algebra): add MonoidHom.coe_id (#21189)
We have this as a @[simp] lemma for most algebraic structures: RingHom, LinearMap, ... I need this for the concrete category refactor, since we will get a lot of @[simp] lemmas about unapplied / partially applied functions, including id.