Commit 2021-02-03 01:05 fcad25f2

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.