surjective Pi.evalMonoidHom

Stream: Is there code for X?

[Jireh Loreaux]

What's the right lemma that's supposed to prove this? Surely we have it.

theorem Pi.surjective_evalMonoidHom {I : Type*} (f : I → Type*) [(i : I) → MulOneClass (f i)]
    (i : I) : Function.Surjective (evalMonoidHom f i) :=
  fun g ↦ ⟨mulSingle i g, by simp⟩

[Yaël Dillies]

docs#Function.surjective_eval ?

[Jireh Loreaux]

Yaël search for the win. I was looking for Pi.surjective_eval.