Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-07-28 (claude-fable-5)
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.

Field

Definition

A field is a set F equipped with two binary operations + (addition) and ⋅ (multiplication) and two distinguished elements 0≠1 of F, satisfying:

  • (A) (F,+) is an abelian group with identity 0: addition is associative and commutative, x+0=x for all x, and every x has an additive inverse −x with x+(−x)=0.
  • (M) Multiplication is associative and commutative on all of F, and x⋅1=x for every x∈F; moreover (F∖{0},⋅) is an abelian group with identity 1, so every x≠0 has a multiplicative inverse x−1 with x⋅x−1=1.
  • (D) Multiplication distributes over addition: x⋅(y+z)=x⋅y+x⋅z.

We write x−y:=x+(−y) and x/y:=x⋅y−1 (for y≠0), and abbreviate x⋅y as xy.

Remarks

  • The rationals Q (The rationals form a field) and both constructions of the reals (The reals form a field, The Dedekind reals form a field) are fields. This definition states the field axioms once, abstractly, so that every field fact proved from them applies to all of these at once.
  • The requirement 0≠1 excludes the trivial one-element structure.
  • Why (M) quantifies over all of F explicitly (amended 2026-07-28, owner approved). An earlier wording headed (M) with the group (F∖{0},⋅) alone, and under that strict reading the axioms do not pin down the products 0⋅y: take F2 and redefine 0⋅y:=y, which leaves (A) untouched, leaves (F∖{0},⋅) the trivial group, and satisfies (D) in all eight instances, yet has 0⋅1=1 — making Multiplication by zero: 0⋅a=0 false in a purported model of the axioms. Associativity, commutativity and x⋅1=x are therefore asserted on all of F, the element 0 included. Commutativity on all of F is also what turns (D) into its right-hand form (y+z)⋅x=y⋅x+z⋅x, which Multiplication by zero: 0⋅a=0 uses.
  • The identities 0,1 and the inverses −x,x−1 are unique (Identities and inverses in a field are unique ↗), so writing them as single-valued notation, and the abbreviations x−y:=x+(−y) and x/y:=xy−1, are legitimate.

Used by

…and 175 more results.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources