Sign function #
This file defines the sign function for types with zero and a decidable less-than relation, and proves some basic theorems about it.
SignType.cast
as a MulWithZeroHom
.
Equations
- SignType.castHom = { toFun := SignType.cast, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
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
)
Equations
- signHom = { toFun := ⇑SignType.sign, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
In this section we explicitly handle universe variables, because Lean creates a fresh universe variable for the type whose existence is asserted. But we want the type to live in the same universe as the input type.
We can decompose a sum of absolute value n
into a sum of n
signs.
We can decompose a sum of absolute value less than n
into a sum of at most n
signs.