feat(algebra/ring): add mk_mul_self_of_two_ne_zero (#5862)
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.





leanprover-community/mathlib,leanprover-community/mathlib