Subset_of_Module_Containing_Zero_is_Linearly_Dependent

Proved

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

linear-algebralinear-independenceproofwiki

Let $G$ be a group whose identity is $e$ . Let $\struct {R, +, \circ}$ be a ring whose zero is $0_R$ . Let $\struct {G, +_G, \circ}_R$ be an $R$ -module. Let $H \subseteq G$ such that $e \in H$ . Then $H$ is a linearly dependent set.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Subset_of_Module_Containing_Zero_is_Linearly_Dependent {R : Type _} [Ring R] [Nontrivial R] {M : Type _} [AddCommGroup M] [Module R M] {S : Set M} (h : (0 : M) ∈ S) : ¬ LinearIndependent R (fun (x : S) => (x : M)) := by sorry

Source

https://proofwiki.org/wiki/Subset_of_Module_Containing_Identity_is_Linearly_Dependent

View graph