Recently, I introduced a global definition for the "Ring of Integers":
df-zring $a |- ZZring = ( CCfld |`s ZZ ) $
Currently, such a definition is used locally in many theorems as
hypothesis, e,g.:
zrhval.1 $e |- Z = ( CCfld |`s ZZ ) $.
zrhval.2 $e |- L = ( ZRHom ` R ) $.
zrhval $p |- L = U. ( Z RingHom R ) $=
Now I want to replace such local definitions by the global one, so that the
previous example would become:
zrhval.2 $e |- L = ( ZRHom ` R ) $.
zrhval $p |- L = U. ( ZZring RingHom R ) $=
By removing the hypothesis, however, the proof of such a theorem becomes
completely invalid! Is there a simple way to perform such a transformation
easily ((almost) automatically at best)? Until now, I rewrote the complete
proofs (which was acceptable since the proofs were not very long, but there
are many theorems to be updated with much longer proofs...).
Alexander
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/84f5417b-7a53-4c78-970a-f1d2eb033165%40googlegroups.com.
