LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

In a module, $0_Rm=0_M$ , $r0_M=0_M$ , $(-r)m=-(rm)$ and $r(-m)=-(rm)$

Statement

For every left $R$ -module $M$ , scalar $r\in R$ , and element $m\in M$ ,

$0_Rm=0_M,\qquad r0_M=0_M,\qquad (-r)m=-(rm),\qquad r(-m)=-(rm).$

Facts & Assumptions

Given: A left $R$ -module $M$ , $r\in R$ , and $m\in M$ .

[L1]

The module action distributes over both addition operations, and $(M,+,0_M)$ is an abelian group (Unital left and right modules over a ring; unqualified module means left module).

[L2]

The additive structure $(R,+,0_R)$ is an abelian group, so $r+(-r)=0_R$ (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[L3]

Cancellation holds in every group, hence in the additive groups of $R$ and $M$ (Cancellation in a group: $gx = gy$ or $xg = yg$ forces $x = y$ ; equivalently left and right translation by $g$ are bijections of $G$ , so $gx = h$ and $xg = h$ each have exactly one solution).

Proof

technique · direct

1.1

Since $0_R=0_R+0_R$ , distributivity gives $0_Rm=0_Rm+0_Rm$ ; cancellation yields $0_Rm=0_M$ .

L1L3given

1.2

Since $0_M=0_M+0_M$ , distributivity gives $r0_M=r0_M+r0_M$ ; cancellation yields $r0_M=0_M$ .

L1L3given

2.1

From $(r+(-r))m=0_Rm=0_M$ , distributivity and step 1.1 give $rm+(-r)m=0_M$ , so $(-r)m=-(rm)$ .

step 1.1L1L2L3given

3.1

From $r(m+(-m))=r0_M=0_M$ , distributivity and step 1.2 give $rm+r(-m)=0_M$ , so $r(-m)=-(rm)$ .

step 1.2L1L3given∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

McGerty, Algebra II: Rings and Modules, Section 3 (standard reference, not scraped)

In a module, 0Rm=0M0_Rm=0_M0R​m=0M​, r0M=0Mr0_M=0_Mr0M​=0M​, (−r)m=−(rm)(-r)m=-(rm)(−r)m=−(rm) and r(−m)=−(rm)r(-m)=-(rm)r(−m)=−(rm)