Alphabeta Math
TheoremStatement: 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.

The quotient action is well defined and makes M/NM/N a module

Statement

Let N≤MN\le M be a submodule of a left RR-module. The rule

r(m+N):=rm+Nr(m+N):=rm+N

is independent of the representative m+Nm+N and, together with the additive quotient group, makes M/NM/N a left RR-module.

Facts & Assumptions

Given: A left RR-module MM and a submodule N≤MN\le M.

[L1]

Additive cosets satisfy m+N=m′+Nm+N=m'+N exactly when m′−m∈Nm'-m\in N (x∈aHx\in aH iff a−1x∈Ha^{-1}x\in H, and aH=bHaH=bH iff a−1b∈Ha^{-1}b\in H).

[L2]

A submodule is closed under scalar multiplication and is an additive subgroup (Submodule of a module).

[L3]

The additive cosets form a quotient group with the inherited addition (For N⊴GN\mathrel{\trianglelefteq}G, the cosets form a group with identity NN and inverse (gN)−1=g−1N(gN)^{-1}=g^{-1}N).

[L4]

The module axioms give distributivity, associativity of scalar action, and 1Rm=m1_Rm=m (Unital left and right modules over a ring; unqualified module means left module).

[L5]

Scalar multiplication preserves additive negatives (In a module, 0Rm=0M0_Rm=0_M, r0M=0Mr0_M=0_M, (−r)m=−(rm)(-r)m=-(rm) and r(−m)=−(rm)r(-m)=-(rm)).

Proof

technique · direct
1.1

If m+N=m′+Nm+N=m'+N, then m′−m∈Nm'-m\in N by [L1]. Thus r(m′−m)=rm′−rm∈Nr(m'-m)=rm'-rm\in N by [L2, L4, L5], and [L1] gives rm+N=rm′+Nrm+N=rm'+N; the proposed scalar action is well defined.

L1L2L4L5given
1.2

The quotient addition is an abelian group operation: it is a quotient-group operation by [L3], and (m+N)+(m′+N)=(m+m′)+N=(m′+m)+N=(m′+N)+(m+N)(m+N)+(m'+N)=(m+m')+N=(m'+m)+N=(m'+N)+(m+N).

L3L4given
1.3

For cosets, the module identities in MM give r((m+N)+(m′+N))=r(m+m′)+N=(rm+rm′)+N=r(m+N)+r(m′+N)r((m+N)+(m'+N))=r(m+m')+N=(rm+rm')+N=r(m+N)+r(m'+N), (r+s)(m+N)=r(m+N)+s(m+N)(r+s)(m+N)=r(m+N)+s(m+N), (rs)(m+N)=r(s(m+N))(rs)(m+N)=r(s(m+N)), and 1R(m+N)=m+N1_R(m+N)=m+N.

L4given
2.1

Steps 1.1--1.3 verify a well-defined scalar action on an abelian group satisfying all module axioms; hence M/NM/N is a left RR-module.

step 1.1step 1.2step 1.3L4∎

Depends on

Used by

Cited to discharge well-definedness by Quotient module M/N with scalar multiplication on additive cosets.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 24 results over 13 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