Prove2Me

Projection_is_Epimorphism

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

direct-productsepimorphismsproofwiki

The projection from an external direct product to a factor is a surjective homomorphism.

Preamble
import Mathlib.Algebra.Group.Prod
Formal statement
theorem Projection_is_Epimorphism {G H : Type _} [Group G] [Group H] : Function.Surjective (MonoidHom.fst G H) := by sorry
Source
https://proofwiki.org/wiki/Projection_is_Epimorphism

View graph