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 field, the additive multiple is the canonical natural : the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion ,
Statement
Let be a field (Field), which is a ring by Every field is a commutative ring with ; it is an integral domain, and it is a commutative division ring. Two functions are in play:
- , the canonical natural of The canonical natural of a field, defined by and ;
- , the additive natural power of the element in the abelian group , defined by Powers : natural exponents in a monoid and integer exponents in a group, with read additively: and .
These are the same function: for every . In particular the notation used by The canonical natural of a field and the notation used by Powers : natural exponents in a monoid and integer exponents in a group, with denote the same element of , and no second notion is in play.
Facts & Assumptions
Given: A field with and , the map of The canonical natural of a field, and the additive natural powers of Powers : natural exponents in a monoid and integer exponents in a group, with in the group .
is a ring, so is an abelian group (Every field is a commutative ring with ; it is an integral domain, and it is a commutative division ring, Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Group and abelian group).
and for every (The canonical natural of a field).
The additive natural powers satisfy and for every and every (Powers : natural exponents in a monoid and integer exponents in a group, with ).
On : and , so (Addition of natural numbers, The natural numbers (von Neumann)).
The recursion theorem: for a set , an element and a function there is exactly one with and (The recursion theorem).
Proof
Let be the function , which is a function from to because addition is a binary operation on . By [L5] applied with , and this , there is exactly one function satisfying and for every .
The map satisfies those two equations: by [L2], and by [L2] together with .
The map satisfies them too: and , both by [L3] with .
By the uniqueness clause of step 1.1, the two functions of steps 1.2 and 1.3 are equal, so for every .
Remarks
-
This is the item the characteristic rests on. The characteristic of a ring: the least with when one exists, and otherwise is stated for an arbitrary ring using the additive powers of Powers : natural exponents in a monoid and integer exponents in a group, with ; for a field a reader may already know The canonical natural of a field, and without the present lemma the page would carry two notations for one element and invite the reader to assume they agree. That assumption is exactly the defect this item removes, and it is removed by a proof rather than by a remark.
-
Uniqueness, not a computation, is what does the work. Both functions are characterised by the same recursion, and The recursion theorem says a recursion of that shape has exactly one solution. An induction on would prove the same thing directly; nothing is gained by writing it out, since the uniqueness clause of The recursion theorem is that induction.
-
contains , and , not . So is not the map " added to itself times" for only: the value at is a genuine value of the recursion. The canonical natural of a field records the same point, and the published Canonical naturals are positive and strictly increasing states its own recursion from , which agrees because .
Depends on
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Powers $g^{n}$: natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$
- Field
- Every field is a commutative ring with $1 \ne 0$; it is an integral domain, and it is a commutative division ring
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
- The recursion theorem
- The natural numbers $\mathbb{N}$ (von Neumann)
- Addition of natural numbers
- Group and abelian group
Used by
- The characteristic of a ring: the least n ≥ 1 with n · 1_R = 0 when one exists, and 0 otherwise Definition
- ℚ and ℝ are fields, hence commutative rings, integral domains and ordered rings, all of characteristic 0 Example
- An additive f : ℝ → ℝ satisfies f(0) = 0, f(-x) = -f(x) and f(qx) = q f(x) for every rational q and every real x; in particular f(q) = q f(1) at every rational q Lemma
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 57 results over 17 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
- Characteristic (algebra) (Wikipedia) (standard reference, not scraped)
- Recursion (Wikipedia) (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.3: Rings (standard reference, not scraped)