New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*/pi): rename *_hom.apply to pi.eval_*_hom #5851
Conversation
d5685d7
to
57630bb
Compare
My only worry is that these names now become quite long. I've regularly used |
Let's see whether CI indicates that code like that has ended up in mathlib. It would certainly help if we had a shorter suffix than |
LGTM the names didn't seem to get much longer, since (at least currently) the namespaces were not opened. bors merge |
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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Naming.3A.20eval.20vs.20apply/near/223813950)
Pull request successfully merged into master. Build succeeded: |
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
orring_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 anadd_monoid_hom
. Using the naming convention established by this commit, that's easy; it'slinear_map.eval_add_monoid_hom
to mirrorpi.apply_add_monoid_hom
.This partially addresses this zulip discussion
Split from #5834