Alphabeta MathHow 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.
and , the arithmetic of and read off the subgroups of
Example
Take and . Then and , and and ; equivalently, in the subgroup generated by is and turns these two numbers into two statements about subgroups of :
The first says that the integers expressible as are exactly the multiples of ; the smallest positive one is . The second says that the integers divisible by both and are exactly the multiples of . The product check is .
Numerals. For the symbol inside means , the embedding of The naturals embed in the integers.
Facts & Assumptions
Given: The integers , , , and , and .
is a commutative ring: multiplication is associative and commutative, , , and multiplication distributes over addition (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).
exactly when , , and every common divisor of and divides (Every common divisor of and divides ; consequently exactly when , , , and every common divisor of and divides — a characterisation that holds at as well, Common divisor, and the greatest common divisor , with the convention ).
If and then for all (Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and ); means for some (Divisibility in : when for some integer ).
, and every common multiple of and is a multiple of (Every common multiple of and is a multiple of , and , Common multiple, and the least common multiple , taken to be when or ).
and , and these are subgroups of ( and ; equivalently, in the subgroup generated by is and , Subgroup, Group and abelian group, The subgroup generated by a subset, the cyclic subgroup , and cyclic groups).
Every subgroup of has exactly one nonnegative generator (Every subgroup of is for exactly one natural number ).
Verification
. Indeed ; and , so and ; and , so every common divisor of and divides by [L3]. By [L2] this characterises .
. By [L4], ; with step 1.1 this reads . Since and , cancellation gives .
Applying [L7] with and : and .
Both right-hand sides are written with their canonical generator: and , and by [L8] no other nonnegative integer generates the same subgroup, so the two identities pin the subgroups down rather than merely exhibiting one description of each.
The two statements read concretely: an integer is of the form exactly when it is a multiple of — with the smallest positive such value — and an integer is divisible by both and exactly when it is a multiple of , which is the divisibility clause of [L4] instantiated here.
Remarks
-
The example is the seam in miniature. On the left of each identity is a construction in the group — a sum of subgroups, an intersection of subgroups — and on the right is a number computed by arithmetic. and ; equivalently, in the subgroup generated by is and is what makes the two sides the same object.
-
, so is visibly a common multiple; what is not visible without the theorem is that every common multiple is a multiple of it, which is why is exactly and not merely contains it.
Depends on
- $a\mathbb{Z} + b\mathbb{Z} = \gcd(a,b)\,\mathbb{Z}$ and $a\mathbb{Z} \cap b\mathbb{Z} = \operatorname{lcm}(a,b)\,\mathbb{Z}$; equivalently, in $(\mathbb{Z},+)$ the subgroup generated by $\{a,b\}$ is $\langle \gcd(a,b) \rangle$ and $\langle a \rangle \cap \langle b \rangle = \langle \operatorname{lcm}(a,b) \rangle$
- Every subgroup of $(\mathbb{Z}, +)$ is $\langle n \rangle = n\mathbb{Z}$ for exactly one natural number $n$
- Every common multiple of $a$ and $b$ is a multiple of $\operatorname{lcm}(a,b)$, and $\gcd(a,b) \cdot \operatorname{lcm}(a,b) = |ab|$
- Common multiple, and the least common multiple $\operatorname{lcm}(a,b)$, taken to be $0$ when $a = 0$ or $b = 0$
- Common divisor, and the greatest common divisor $\gcd(a,b)$, with the convention $\gcd(0,0) := 0$
- Every common divisor of $a$ and $b$ divides $\gcd(a,b)$; consequently $d = \gcd(a,b)$ exactly when $d \ge 0$, $d \mid a$, $d \mid b$, and every common divisor of $a$ and $b$ divides $d$ — a characterisation that holds at $(a,b) = (0,0)$ as well
- Divisibility is reflexive and transitive on $\mathbb{Z}$, and is linear: if $d \mid a$ and $d \mid b$ then $d \mid ax + by$ for all integers $x, y$; also $d \mid a$ implies $d \mid ac$, $-d \mid a$ and $d \mid -a$
- Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$
- Subgroup
- The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$, and cyclic groups
- Group and abelian group
- The integers have no zero divisors; multiplicative cancellation
- The absolute value $|a|$ of an integer
- Absolute value in $\mathbb{Z}$: $|a| \ge 0$; $|a| = 0$ exactly when $a = 0$; $|-a| = |a|$; $|ab| = |a|\,|b|$; $-|a| \le a \le |a|$; and $|a| \le c$ exactly when $-c \le a \le c$
- The integers form a commutative ring
- Arithmetic on the integers
- The naturals embed in the integers
- The integers as equivalence classes of pairs of naturals
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Cyclic group (Wikipedia) (standard reference, not scraped)
- Bézout's identity (Wikipedia) (standard reference, not scraped)
- Least common multiple (Wikipedia) (standard reference, not scraped)