Step * of Lemma rng_all_properties

[r:Rng]. (Assoc(|r|;+r) ∧ Ident(|r|;+r;0) ∧ Inverse(|r|;+r;0;-r) ∧ Assoc(|r|;*) ∧ Ident(|r|;*;1) ∧ BiLinear(|r|;+r;*))
BY
THENM (D 1) THENA Auto }

1
1. RngSig
2. IsRing(|r|;+r;0;-r;*;1)
⊢ Assoc(|r|;+r) ∧ Ident(|r|;+r;0) ∧ Inverse(|r|;+r;0;-r) ∧ Assoc(|r|;*) ∧ Ident(|r|;*;1) ∧ BiLinear(|r|;+r;*)


Latex:


Latex:
\mforall{}[r:Rng]
    (Assoc(|r|;+r)
    \mwedge{}  Ident(|r|;+r;0)
    \mwedge{}  Inverse(|r|;+r;0;-r)
    \mwedge{}  Assoc(|r|;*)
    \mwedge{}  Ident(|r|;*;1)
    \mwedge{}  BiLinear(|r|;+r;*))


By


Latex:
D  0  THENM  (D  1)  THENA  Auto




Home Index