Definition elimination contest

Stream: general

[Eric Wieser]

We currently have both docs#distrib_mul_action.to_add_monoid_hom and docs#const_smul_hom. They're defeq:

import algebra.group_ring_action

example {M A: Type*} [monoid M] [add_monoid A] [distrib_mul_action M A] :
  distrib_mul_action.to_add_monoid_hom M A = const_smul_hom A := rfl

[Eric Wieser]

/poll Which should be be removed?

• distrib_mul_action.to_add_monoid_hom R M
• const_smul_hom M

[Eric Wieser]

Note we have docs#mul_action.to_perm and docs#distrib_mul_action.to_add_equiv which sort of fits the pattern of the former. On the other hand, I feel like the latter is way more discoverable, and matches docs#smul_add_hom

[Eric Wieser]

@Scott Morrison, @Oliver Nash: if you're in favor of removing const_smul_hom, would you rename docs#smul_add_hom to module.to_add_monoid_hom?

[Oliver Nash]

Yeah I think so.

[Johan Commelin]

Hmm, I don't really like those long names

[Johan Commelin]

Can't we have const_smul_hom and smul_add_hom as aliases or something?

[Eric Wieser]

That or abbreviations, yeah.

[Eric Wieser]

I somewhat ignored the vote in this thread (mainly because I forgot about it until after I made the change), but #8953 removes const_smul_hom. It's rarely used anyway, so I think it's not really worth worrying about the name.

[Eric Wieser]

I totally misread the vote upthread, we were voting for which one to remove not which one to keep; so the PR is inline with the 4 month old opinions.