Sign type

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

inductive SignType : Type

The type of signs.

• zero : SignType
• neg : SignType
• pos : SignType

instance instDecidableEqSignType : DecidableEq SignType

Equations

• instDecidableEqSignType x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance instInhabitedSignType : Inhabited SignType

Equations

• instInhabitedSignType = { default := SignType.zero }

instance instFintypeSignType : Fintype SignType

Equations

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

instance SignType.instZero : Zero SignType

Equations

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

instance SignType.instOne : One SignType

Equations

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

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 }

@[simp]

theorem SignType.zero_eq_zero : zero = 0

@[simp]

theorem SignType.neg_eq_neg_one : neg = -1

@[simp]

theorem SignType.pos_eq_one : pos = 1

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 }

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

instance SignType.instLE : LE SignType

Equations

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

instance SignType.LE.decidableRel : DecidableRel SignType.LE

Equations

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

instance SignType.decidableEq : DecidableEq SignType

Equations

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

instance SignType.instCommGroupWithZero : CommGroupWithZero SignType

Equations

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

instance SignType.instLinearOrder : LinearOrder SignType

Equations

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

instance SignType.instBoundedOrder : BoundedOrder SignType

Equations

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

instance SignType.instHasDistribNeg : HasDistribNeg SignType

Equations

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

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.

theorem SignType.nonneg_iff {a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1

theorem SignType.nonneg_iff_ne_neg_one {a : SignType} : 0 ≤ a ↔ a ≠ -1

theorem SignType.neg_one_lt_iff {a : SignType} : -1 < a ↔ 0 ≤ a

theorem SignType.nonpos_iff {a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0

theorem SignType.nonpos_iff_ne_one {a : SignType} : a ≤ 0 ↔ a ≠ 1

theorem SignType.lt_one_iff {a : SignType} : a < 1 ↔ a ≤ 0

@[simp]

theorem SignType.neg_iff {a : SignType} : a < 0 ↔ a = -1

@[simp]

theorem SignType.le_neg_one_iff {a : SignType} : a ≤ -1 ↔ a = -1

@[simp]

theorem SignType.pos_iff {a : SignType} : 0 < a ↔ a = 1

@[simp]

theorem SignType.one_le_iff {a : SignType} : 1 ≤ a ↔ a = 1

@[simp]

theorem SignType.neg_one_le (a : SignType) : -1 ≤ a

@[simp]

theorem SignType.le_one (a : SignType) : a ≤ 1

@[simp]

theorem SignType.not_lt_neg_one (a : SignType) : ¬a < -1

@[simp]

theorem SignType.not_one_lt (a : SignType) : ¬1 < a

@[simp]

theorem SignType.self_eq_neg_iff {a : SignType} : a = -a ↔ a = 0

@[simp]

theorem SignType.neg_eq_self_iff {a : SignType} : -a = a ↔ a = 0

@[simp]

theorem SignType.neg_eq_zero_iff {a : SignType} : -a = 0 ↔ a = 0

@[simp]

theorem SignType.neg_one_lt_one : -1 < 1

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

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 }

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.

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.

@[simp]

theorem SignType.coe_zero {α : Type u_1} [Zero α] [One α] [Neg α] : ↑0 = 0

@[simp]

theorem SignType.coe_one {α : Type u_1} [Zero α] [One α] [Neg α] : ↑1 = 1

@[simp]

theorem SignType.coe_neg_one {α : Type u_1} [Zero α] [One α] [Neg α] : ↑(-1) = -1

@[simp]

theorem SignType.coe_neg {α : Type u_2} [One α] [SubtractionMonoid α] (s : SignType) : ↑(-s) = -↑s

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' := ⋯ }

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

@[simp]

theorem sign_zero {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] : SignType.sign 0 = 0

@[simp]

theorem sign_pos {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : 0 < a) : SignType.sign a = 1

@[simp]

theorem sign_neg {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : a < 0) : SignType.sign a = -1

theorem sign_eq_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = 1 ↔ 0 < a

theorem sign_eq_neg_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = -1 ↔ a < 0

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.

@[simp]

theorem sign_eq_zero_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a = 0 ↔ a = 0

theorem sign_ne_zero {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a ≠ 0 ↔ a ≠ 0

@[simp]

theorem sign_nonneg_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : 0 ≤ SignType.sign a ↔ 0 ≤ a

@[simp]

theorem sign_nonpos_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : SignType.sign a ≤ 0 ↔ a ≤ 0

theorem sign_one {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [DecidableLT α] [Nontrivial α] : SignType.sign 1 = 1

theorem Left.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddLeftStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a

theorem Right.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddRightStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a

theorem Int.sign_eq_sign (n : ℤ) : n.sign = ↑(SignType.sign n)