Linear_Transformation_of_Generated_Module

Proved

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

linear-algebralinear-transformationsmodulesproofwiki

Let $G$ and $H$ be $R$ -modules. Let $\phi$ and $\psi$ be linear transformations $G$ into $H$ . Let $S$ be a generator for $G$ . Suppose that $\forall x \in S: \map \phi x = \map \psi x$ . Then $\phi = \psi$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Linear_Transformation_of_Generated_Module {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (phi psi : M →ₗ[R] N) (S : Set M) (h : forall s, s ∈ S -> phi s = psi s) : forall x, x ∈ Submodule.span R S -> phi x = psi x := by sorry

Source

https://proofwiki.org/wiki/Linear_Transformation_of_Generated_Module

View graph