Nuprl Lemma : p-mul-comm
∀[p:{2...}]. ∀[x,y:p-adics(p)]. (x * y = y * x ∈ p-adics(p))
Proof
Definitions occuring in Statement :
p-mul: x * y,
p-adics: p-adics(p),
int_upper: {i...},
uall: ∀[x:A]. B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
crng: CRng,
rng: Rng,
p-adic-ring: ℤ(p),
ring_p: IsRing(T;plus;zero;neg;times;one),
rng_car: |r|,
pi1: fst(t),
rng_plus: +r,
pi2: snd(t),
rng_zero: 0,
rng_minus: -r,
rng_times: *,
rng_one: 1,
monoid_p: IsMonoid(T;op;id),
group_p: IsGroup(T;op;id;inv),
bilinear: BiLinear(T;pl;tm),
ident: Ident(T;op;id),
assoc: Assoc(T;op),
inverse: Inverse(T;op;id;inv),
infix_ap: x f y,
comm: Comm(T;op)
Lemmas referenced :
p-adic-ring_wf,
crng_properties,
rng_properties,
int_upper_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
applyLambdaEquality,
setElimination,
rename,
sqequalRule,
natural_numberEquality
Latex:
\mforall{}[p:\{2...\}]. \mforall{}[x,y:p-adics(p)]. (x * y = y * x)
Date html generated:
2018_05_21-PM-03_21_01
Last ObjectModification:
2018_05_19-AM-08_18_18
Theory : rings_1
Home
Index