English
The sign function extends to a monoid-with-zero homomorphism from α to SignType, preserving multiplication and mapping 0 → 0 and 1 → 1.
Русский
Функция sign расширяет до гомоморфизма моноида с нулём от α к SignType, сохраняющего умножение и отправляющего 0 в 0, 1 в 1.
LaTeX
$$$\text{signHom} : \alpha \to_{\_0} SignType$ with $\text{sign}(ab)=\text{sign}(a)\text{sign}(b)$, $\text{sign}(0)=0$, $\text{sign}(1)=1$$$
Lean4
/-- `SignType.sign` as a `MonoidWithZeroHom` for a nontrivial ordered semiring. Note that linearity
is required; consider ℂ with the order `z ≤ w` iff they have the same imaginary part and
`z - w ≤ 0` in the reals; then `1 + I` and `1 - I` are incomparable to zero, and thus we have:
`0 * 0 = SignType.sign (1 + I) * SignType.sign (1 - I) ≠ SignType.sign 2 = 1`.
(`Complex.orderedCommRing`) -/
def signHom : α →*₀ SignType where
toFun := sign
map_zero' := sign_zero
map_one' := sign_one
map_mul' := sign_mul
