Elements_Equal_Images_Linear_Transformations_form_Submodule

Proved

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

linear-algebralinear-transformationsmodulesproofwikisubmodules

Let $G$ and $H$ be $R$ -modules. Let $\phi$ and $\psi$ be linear transformations from $G$ into $H$ . Then the set $S = \set {x \in G: \map \phi x = \map \psi x}$ is a submodule of $G$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Elements_Equal_Images_Linear_Transformations_form_Submodule {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (phi psi : M →ₗ[R] N) : ∃ (S : Submodule R M), (S : Set M) = {x | phi x = psi x} := by sorry

Source

https://proofwiki.org/wiki/Elements_of_Module_with_Equal_Images_under_Linear_Transformations_form_Submodule

View graph