Condition_for_Linear_Transformation

Proved

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

linear-transformationsmodule-theoryproofwiki

Let $G$ be a unitary $R$ -module, and let $H$ be an $R$ -module. Let $\phi: G \to H$ be a mapping. Then $\phi$ is a linear transformation $\forall x, y \in G: \forall \lambda, \mu \in R: \map \phi {\lambda x + \mu y} = \lambda \map \phi x + \mu \map \phi y$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Condition_for_Linear_Transformation {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M → N) (hf_add : ∀ x y : M, f (x + y) = f x + f y) (hf_smul : ∀ (r : R) (x : M), f (r • x) = r • f x) : ∃ g : M →ₗ[R] N, (g : M → N) = f := by sorry

Source

https://proofwiki.org/wiki/Condition_for_Linear_Transformation

View graph