Commit 2021-05-15 21:20 57b0e68f

chore(*/pi): rename hom.apply to pi.eval_hom (#5851) These definitions state the fact that fixing an i and applying a function (Π i, f i) maintains the algebraic structure of the function. We already have a name for this operation, function.eval. These isn't a statement about monoid_hom or ring_hom at all - that just happens to be their type. For this reason, this commit moves all the definitions of this type into the pi namespace:

• add_monoid_hom.apply → pi.eval_add_monoid_hom
• monoid_hom.apply → pi.eval_monoid_hom
• ring_hom.apply → pi.eval_ring_hom
• pi.alg_hom.apply [sic] → pi.eval_alg_hom This scales better, because we might want to say that applying a linear_map over a non-commutative ring is an add_monoid_hom. Using the naming convention established by this commit, that's easy; it's linear_map.eval_add_monoid_hom to mirror pi.apply_add_monoid_hom. This partially addresses this zulip discussion