feat(algebra/ring): add mk_mul_self_of_two_ne_zero (#5862)
Which allows us to make a ring homomorphism from an additive hom which maps squares to squares assuming a couple of things, this is especially useful in ordered fields where it allows us to think only of positive elements.
