Description: Show that the ring homomorphism in rhmpsr preserves multiplication. (Contributed by SN, 18-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rhmcomulpsr.p | |
|
rhmcomulpsr.q | |
||
rhmcomulpsr.b | |
||
rhmcomulpsr.c | |
||
rhmcomulpsr.1 | |
||
rhmcomulpsr.2 | |
||
rhmcomulpsr.h | |
||
rhmcomulpsr.f | |
||
rhmcomulpsr.g | |
||
Assertion | rhmcomulpsr | |