Induced_Structure_Identity
Provedidentity-elementspointwise-operationsproofwiki
If e is the identity for T, then the constant function mapping everything to e is the identity for the induced pointwise operation on T^S.
Preamble
import Mathlib.Algebra.Group.Pi.Basic
Formal statement
theorem Induced_Structure_Identity {S T : Type _} [Monoid T] : (fun _ : S => (1 : T)) = (1 : S → T) := by sorrySource