Z_of_int and int_of_Z are ring morphisms

theories/ssrZ.v

@@ -111,6 +111,34 @@ Canonical Z_numDomaZype := NumDomainType Z Mixin.
 Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
 Canonical Z_realDomaZype := [realDomainType of Z].
 
+Lemma Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
+Proof.
+have Hnat (m : nat) : Z.of_nat m = (m%:R)%R.
+  by elim: m => // m; rewrite Nat2Z.inj_succ -Z.add_1_l mulrS => ->.
+case: n => n; rewrite /intmul /=; first exact: Hnat.
+by congr Z.opp; rewrite Nat2Z.inj_add /= mulrSr Hnat.
+Qed.
+
+Lemma Z_of_int_is_additive : additive Z_of_int.
+Proof. by move=> m n; rewrite !Z_of_intE raddfB. Qed.
+
+Canonical Z_of_int_additive := Additive Z_of_int_is_additive.
+
+Lemma int_of_Z_is_additive : additive int_of_Z.
+Proof. exact: can2_additive Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_additive := Additive int_of_Z_is_additive.
+
+Lemma Z_of_int_is_multiplicative : multiplicative Z_of_int.
+Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
+
+Canonical Z_of_int_multiplicative := AddRMorphism Z_of_int_is_multiplicative.
+
+Lemma int_of_Z_is_multiplicative : multiplicative int_of_Z.
+Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_multiplicative := AddRMorphism int_of_Z_is_multiplicative.
+
 End ZInstances.
 
 Canonical ZInstances.Z_eqType.
@@ -135,3 +163,7 @@ Canonical ZInstances.Z_orderType.
 Canonical ZInstances.Z_numDomaZype.
 Canonical ZInstances.Z_normedZmodType.
 Canonical ZInstances.Z_realDomaZype.
+Canonical ZInstances.Z_of_int_additive.
+Canonical ZInstances.int_of_Z_additive.
+Canonical ZInstances.Z_of_int_multiplicative.
+Canonical ZInstances.int_of_Z_multiplicative.