commutativity of ring is invariant under isomorphism

[icecream17]

(and elfvunirn)

mathbox only edit: Not mathbox only

[tirix]

Nice!

[icecream17]

draft: ressbasss2 has an extra hypothesis (edit: done)

[langgerard]

In fact, more generally, let A and B be two magmas and H a magma homomorphism (meaning a function from A into B with
H(a.b) = H(a).H(b), then if a and b commute in A, H(a) and H(b)commute in B because H().H(b) = H(a.b) = H(b.a) =H(b).H(a)
So if A is a commutative magma, its image H(A) will be a stable and commutative subset for H in B (so a commutative submagma of B). So that, if A and B are pseudo-rings (meaning rings maybe without a multiplicative unit) and H a pseudo-ring homomorphism (meaning a ring homomorphism without the condition H(1A) = 1B), and if A is commutative, then H(A) will also be a commutative sub pseudo-ring in B.
Moreover, if the magma A has a unit, the submagma H(A) of B will also have H(1) as a unit (than is not necessarily unit for B),
because H(a).H(1) = H(a) = H(1).H(a). So that if A is a (unital) ring, B a pseudo-ring and H a pseudo-ring homomorphism from A into B, H(A) will be a sub pseudo-ring of B with a unit, but because H(1A) is not necessarily a unit for B, H(A) will be a subring of B and H will be a ring-homomorphism from A into B only in the case that H(1A) is a unit for B, that will then be a ring.

[icecream17]

I think everything is finally addressed. Unless something comes up, the only commit left to do is to resolve conflicts after #4553 is merged done