Canonical_Injection_into_Cartesian_Product_of_Modules
Provedcartesian-productlinear-algebramodulesproofwiki
Let be the cartesian product of a sequence of -modules. Then for each , the canonical injection from into is a monomorphism.
Preamble
import Mathlib.LinearAlgebra.Pi
Formal statement
theorem Canonical_Injection_into_Cartesian_Product_of_Modules {R : Type _} [CommRing R] {ι : Type _} (G : ι → Type _) [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)] (j : ι) : ∃ (f : G j →ₗ[R] (∀ i, G i)), Function.Injective f := by sorrySource