# Sign type #

This file defines the type of signs $\{-1, 0, 1\}$ and its basic arithmetic instances.

source
inductive SignType :
Type

The type of signs.

- zero : SignType
- neg : SignType
- pos : SignType

Instances For

source
instance instDecidableEqSignType :
DecidableEq SignType
Equations

- instDecidableEqSignType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
def instInhabitedSignType.default :
SignType
Equations

- instInhabitedSignType.default = SignType.zero

Instances For

source
instance instInhabitedSignType :
Inhabited SignType
Equations

- instInhabitedSignType = { default := instInhabitedSignType.default }

source
instance instFintypeSignType :
Fintype SignType
Equations

- instFintypeSignType = { elems := { val := ↑SignType.enumList, nodup := SignType.enumList_nodup }, complete := instFintypeSignType._proof_1 }

source
instance SignType.instZero :
Zero SignType
Equations

- SignType.instZero = { zero := SignType.zero }

source
instance SignType.instOne :
One SignType
Equations

- SignType.instOne = { one := SignType.pos }

source
instance SignType.instNeg :
Neg SignType
Equations

- SignType.instNeg = { neg := fun (s : SignType) => match s with | SignType.neg => SignType.pos | SignType.zero => SignType.zero | SignType.pos => SignType.neg }

source
@[simp]
theorem SignType.zero_eq_zero :
zero = 0
source
@[simp]
theorem SignType.neg_eq_neg_one :
neg = -1
source
@[simp]
theorem SignType.pos_eq_one :
pos = 1
source
theorem SignType.trichotomy (a : SignType) :
a = -1 ∨ a = 0 ∨ a = 1
source
instance SignType.instMul :
Mul SignType
Equations

- SignType.instMul = { mul := fun (x y : SignType) => match x with | SignType.neg => -y | SignType.zero => SignType.zero | SignType.pos => y }

source
inductive SignType.LE :
SignType → SignType → Prop

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

source
instance SignType.instLE :
LE SignType
Equations

- SignType.instLE = { le := SignType.LE }

source
instance SignType.LE.decidableRel :
DecidableRel SignType.LE
Equations

- One or more equations did not get rendered due to their size.

source
instance SignType.instCommGroupWithZero :
CommGroupWithZero SignType
Equations

- One or more equations did not get rendered due to their size.

source
instance SignType.instLinearOrder :
LinearOrder SignType
Equations

- One or more equations did not get rendered due to their size.

source
instance SignType.instBoundedOrder :
BoundedOrder SignType
Equations

- SignType.instBoundedOrder = { top := 1, le_top := SignType.LE.of_pos, bot := -1, bot_le := SignType.LE.of_neg }

source
instance SignType.instHasDistribNeg :
HasDistribNeg SignType
Equations

- One or more equations did not get rendered due to their size.

source
def SignType.fin3Equiv :
SignType ≃* Fin 3

`SignType` is equivalent to `Fin 3`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem SignType.nonneg_iff {a : SignType} :
0 ≤ a ↔ a = 0 ∨ a = 1
source
theorem SignType.nonneg_iff_ne_neg_one {a : SignType} :
0 ≤ a ↔ a ≠ -1
source
theorem SignType.neg_one_lt_iff {a : SignType} :
-1 < a ↔ 0 ≤ a
source
theorem SignType.nonpos_iff {a : SignType} :
a ≤ 0 ↔ a = -1 ∨ a = 0
source
theorem SignType.nonpos_iff_ne_one {a : SignType} :
a ≤ 0 ↔ a ≠ 1
source
theorem SignType.lt_one_iff {a : SignType} :
a < 1 ↔ a ≤ 0
source
@[simp]
theorem SignType.neg_iff {a : SignType} :
a < 0 ↔ a = -1
source
@[simp]
theorem SignType.le_neg_one_iff {a : SignType} :
a ≤ -1 ↔ a = -1
source
@[simp]
theorem SignType.pos_iff {a : SignType} :
0 < a ↔ a = 1
source
@[simp]
theorem SignType.one_le_iff {a : SignType} :
1 ≤ a ↔ a = 1
source
@[simp]
theorem SignType.neg_one_le (a : SignType) :
-1 ≤ a
source
@[simp]
theorem SignType.le_one (a : SignType) :
a ≤ 1
source
@[simp]
theorem SignType.not_lt_neg_one (a : SignType) :
¬a < -1
source
@[simp]
theorem SignType.not_one_lt (a : SignType) :
¬1 < a
source
@[simp]
theorem SignType.self_eq_neg_iff {a : SignType} :
a = -a ↔ a = 0
source
@[simp]
theorem SignType.neg_eq_self_iff {a : SignType} :
-a = a ↔ a = 0
source
@[simp]
theorem SignType.neg_eq_zero_iff {a : SignType} :
-a = 0 ↔ a = 0
source
@[simp]
theorem SignType.neg_one_lt_one :
-1 < 1
source
def SignType.cast {α : Type u_1} [Zero α] [One α] [Neg α] :
SignType → α

Turn a `SignType` into zero, one, or minus one. This is a coercion instance.

Equations

- ↑SignType.zero = 0
- ↑SignType.pos = 1
- ↑SignType.neg = -1

Instances For

source
instance SignType.instCoeTail {α : Type u_1} [Zero α] [One α] [Neg α] :
CoeTail SignType α

This is a `CoeTail` since the type on the right (trivially) determines the type on the left.

`outParam`-wise it could be a `Coe`, but we don't want to try applying this instance for a coercion to any `α`.

Equations

- SignType.instCoeTail = { coe := SignType.cast }

source
theorem SignType.map_cast' {α : Type u_1} [Zero α] [One α] [Neg α] {β : Type u_2} [One β] [Neg β] [Zero β] (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) :
f ↑s = ↑s

Casting out of `SignType` respects composition with functions preserving `0, 1, -1`.

source
theorem SignType.map_cast {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType) :
f ↑s = ↑s

Casting out of `SignType` respects composition with suitable bundled homomorphism types.

source
@[simp]
theorem SignType.coe_zero {α : Type u_1} [Zero α] [One α] [Neg α] :
↑0 = 0
source
@[simp]
theorem SignType.coe_one {α : Type u_1} [Zero α] [One α] [Neg α] :
↑1 = 1
source
@[simp]
theorem SignType.coe_neg_one {α : Type u_1} [Zero α] [One α] [Neg α] :
↑(-1) = -1
source
@[simp]
theorem SignType.coe_neg {α : Type u_2} [One α] [SubtractionMonoid α] (s : SignType) :
↑(-s) = -↑s
source
def SignType.sign {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] :
α →o SignType

The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.

Equations

- SignType.sign = { toFun := fun (a : α) => if 0 < a then 1 else if a < 0 then -1 else 0, monotone' := ⋯ }

Instances For

source
theorem sign_apply {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
source
@[simp]
theorem sign_zero {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] :
SignType.sign 0 = 0
source
@[simp]
theorem sign_pos {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : 0 < a) :
SignType.sign a = 1
source
@[simp]
theorem sign_neg {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : a < 0) :
SignType.sign a = -1
source
theorem sign_eq_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
SignType.sign a = 1 ↔ 0 < a
source
theorem sign_eq_neg_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
SignType.sign a = -1 ↔ a < 0
source
theorem StrictMono.sign_comp {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} {F : Type u_3} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono ⇑f) (a : α) :
SignType.sign (f a) = SignType.sign a

`SignType.sign` respects strictly monotone zero-preserving maps.

source
@[simp]
theorem sign_eq_zero_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} :
SignType.sign a = 0 ↔ a = 0
source
theorem sign_ne_zero {α : Type u_1} [Zero α] [LinearOrder α] {a : α} :
SignType.sign a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem sign_nonneg_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} :
0 ≤ SignType.sign a ↔ 0 ≤ a
source
@[simp]
theorem sign_nonpos_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} :
SignType.sign a ≤ 0 ↔ a ≤ 0
source
theorem sign_eq_sign_or_eq_neg {α : Type u_1} [Zero α] [LinearOrder α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
SignType.sign a = SignType.sign b ∨ SignType.sign a = -SignType.sign b
source
theorem sign_one {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [DecidableLT α] [Nontrivial α] :
SignType.sign 1 = 1
source
theorem Left.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddLeftStrictMono α] (a : α) :
SignType.sign (-a) = -SignType.sign a
source
theorem Right.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddRightStrictMono α] (a : α) :
SignType.sign (-a) = -SignType.sign a
source
theorem Int.sign_eq_sign (n : ℤ) :
n.sign = ↑(SignType.sign n)