Homomorphism_of_External_Direct_Products
Proveddirect-productshomomorphismsproofwiki
The componentwise application of homomorphisms preserves the product structure on external direct products.
Preamble
import Mathlib.Algebra.Group.Prod import Mathlib.Algebra.Group.Hom.Defs
Formal statement
theorem Homomorphism_of_External_Direct_Products {G₁ G₂ H₁ H₂ : Type _} [Group G₁] [Group G₂] [Group H₁] [Group H₂] (f₁ : MonoidHom G₁ H₁) (f₂ : MonoidHom G₂ H₂) (a b : G₁ × G₂) : (f₁ (a * b).1, f₂ (a * b).2) = (f₁ a.1 * f₁ b.1, f₂ a.2 * f₂ b.2) := by sorrySource