Projection_on_Cartesian_Product_of_Modules

Proved

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

cartesian-productsmodule-theorymodulesprojectionsproofwiki

Let $G$ be the cartesian product of a sequence $\sequence {G_n}$ of $R$ -modules. Then for each $j \in \closedint 1 n$ , the projection $\pr_j$ on the $j$ th co-ordinate is an epimorphism from $G$ onto $G_j$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Projection_on_Cartesian_Product_of_Modules {R : Type _} [Ring R] {n : ℕ} {M : Fin n → Type _} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] (j : Fin n) : ∃ f : (∀ i, M i) →ₗ[R] M j, ∀ x, f x = x j := by sorry

Source

https://proofwiki.org/wiki/Projection_on_Cartesian_Product_of_Modules

View graph