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.
The less-than-or-equal relation on signs.
- of_neg (a : SignType) : neg.LE a
- zero : SignType.zero.LE SignType.zero
- of_pos (a : SignType) : a.LE pos
Instances For
Casting out of SignType
respects composition with suitable bundled homomorphism types.
The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.
Equations
Instances For
SignType.sign
respects strictly monotone zero-preserving maps.
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
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.