f x = 1 for subsingletons

Stream: Is there code for X?

[Eric Rodriguez]

@[to_additive] lemma map_monoid_hom_of_subsingleton {R S F} [mul_one_class R]
  [mul_one_class S] [monoid_hom_class F R S] [subsingleton R] (f : F) (a : R) : f a = 1 :=
(subsingleton.elim 1 a) ▸ map_one f

do we have this already? I don't really like this name, what should I call it?

The things I do for nontriviality to work smoothly...

[Yaël Dillies]

Some inspiration: docs#norm_of_subsingleton