Submodule_Test

Proved

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

linear-algebramodulesproofwikisubmodules

Let $\left({G, +, \circ}\right)_R$ be a unitary $R$ -module. Let $H$ be a non-empty subset of $G$ . Then $\left({H, +, \circ}\right)_R$ is a submodule of $G$ iff $\forall x, y \in H: \forall \lambda \in R: x + y \in H, \lambda \circ x \in H$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Submodule_Test {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] (H : Set M) (hne : H.Nonempty) (hadd : forall x y, x ∈ H -> y ∈ H -> x + y ∈ H) (hsmul : forall (r : R) x, x ∈ H -> r • x ∈ H) : ∃ (S : Submodule R M), (S : Set M) = H := by sorry

Source

https://proofwiki.org/wiki/Submodule_Test

View graph