Step
*
of Lemma
int-to-ring-minus-one
No Annotations
∀[r:Rng]. (int-to-ring(r;-1) = (-r 1) ∈ |r|)
BY
{ (RepUR ``int-to-ring rng_nat_op mon_nat_op nat_op`` 0
THEN RepeatFor 2 ((RecUnfold `itop` 0 THEN Reduce 0 THEN Auto))
) }
Latex:
Latex:
No Annotations
\mforall{}[r:Rng]. (int-to-ring(r;-1) = (-r 1))
By
Latex:
(RepUR ``int-to-ring rng\_nat\_op mon\_nat\_op nat\_op`` 0
THEN RepeatFor 2 ((RecUnfold `itop` 0 THEN Reduce 0 THEN Auto))
)
Home
Index