mathlib3

2230ae61 - feat(data/sign): `sign_one`, `sign_mul`, `sign_pow` (#16058)

feat(data/sign): `sign_one`, `sign_mul`, `sign_pow` (#16058) Add a lemma about the sign of the product of two numbers (in the `linear_ordered_ring` case, extracted from the existing `sign_hom` in that case). Also add `sign_one` and `sign_pow`.