Epimorphism_preserves_Modules

Proved

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

epimorphismsmodule-theorymodulesproofwiki

Let $\left({G, +_G, \circ}\right)_R$ be an $R$ -module. Let $\left({H, +_H, \circ}\right)_R$ be an $R$ -algebraic structure. Let $\phi: G \to H$ be an epimorphism. Then $H$ is an $R$ -module.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Epimorphism_preserves_Modules {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective f) : ∀ r : R, ∀ n : N, ∃ m : M, f (r • m) = r • n := by sorry

Source

https://proofwiki.org/wiki/Epimorphism_preserves_Modules

View graph