Product of multiplicative function on Lists

Stream: Is there code for X?

[Gareth Ma]

Does the following theorem exist?

example [Monoid α] [Monoid β]
    (f : α → β) (hf : ∀ a b, f (a * b) = f a * f b) (h1 : f 1 = 1) (l : List α) :
    (l.map f).prod = f l.prod := by
  exact?

(Here's a proof:

example [Monoid α] [Monoid β]
    (f : α → β) (hf : ∀ a b, f (a * b) = f a * f b) (h1 : f 1 = 1) (l : List α) :
    (l.map f).prod = f l.prod := by
  induction' l with l ls ih
  · simp only [List.prod, List.map_nil, List.foldl_nil, h1]
  · rw [List.map_cons, List.prod_cons, List.prod_cons, hf, ih]

) Feels significant enough to be included.

[Eric Wieser]

docs#map_list_prod

[Gareth Ma]

Ah, they used MonoidHomClass. Thanks.

[Eric Wieser]

import Mathlib.Data.List.BigOperators.Basic

example [Monoid α] [Monoid β]
    (f : α → β) (hf : ∀ a b, f (a * b) = f a * f b) (h1 : f 1 = 1) (l : List α) :
    (l.map f).prod = f l.prod :=
  Eq.symm <| map_list_prod { toFun := f, map_one' := h1, map_mul' := hf : _ →* _} l

[Yury G. Kudryashov]

Should this map_list_prod be formulated for a MulOneClass instead of Monoid?