/sci/ - Science & Math

ive always wondered if the field axiom 0 =/= 1 is redundant.

if you have the definitions for additive inverse, 0 and 1, distributivity and commutativity, then you get

[math]
1a=a,\space a+0=a\\
1a=a \implies (1+0)a=a\\
\implies 1a + 0a = a\\
\implies 1a+0a-1a=0a=a-1a=0\\
\implies 0a = 0
[/math]

this isnt the law for 1a=a unless a must be 0, but a is an arbitrary element of the field
so either a field has one element (which is 0 and 1), or 0=/=1 in the field.

the reason people seem to say that a 1 element field doesnt exist is because 0 and 1 need to be distinct, but in this context thats just circular

so it seems redundant to add this axiom since its inherent in any field with more than 1 element, but ive seen it in every single field definition. Do you guys know of any reason for that? or did i just fuck up in the steps somewhere