mathlib documentation

data.sign

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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
inductive sign_type.le  :
sign_typesign_type → Prop

The less-than relation on signs.

Instances for sign_type.le
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • sign_type.comm_group_with_zero = {mul := has_mul.mul sign_type.has_mul, mul_assoc := sign_type.comm_group_with_zero._proof_1, one := 1, one_mul := sign_type.comm_group_with_zero._proof_2, mul_one := sign_type.comm_group_with_zero._proof_3, npow := comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5, npow_zero' := sign_type.comm_group_with_zero._proof_6, npow_succ' := sign_type.comm_group_with_zero._proof_7, mul_comm := sign_type.comm_group_with_zero._proof_8, zero := 0, zero_mul := sign_type.comm_group_with_zero._proof_9, mul_zero := sign_type.comm_group_with_zero._proof_10, inv := id sign_type, div := group_with_zero.div._default has_mul.mul sign_type.comm_group_with_zero._proof_11 1 sign_type.comm_group_with_zero._proof_12 sign_type.comm_group_with_zero._proof_13 (comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5) sign_type.comm_group_with_zero._proof_14 sign_type.comm_group_with_zero._proof_15 id, div_eq_mul_inv := sign_type.comm_group_with_zero._proof_16, zpow := group_with_zero.zpow._default has_mul.mul sign_type.comm_group_with_zero._proof_17 1 sign_type.comm_group_with_zero._proof_18 sign_type.comm_group_with_zero._proof_19 (comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5) sign_type.comm_group_with_zero._proof_20 sign_type.comm_group_with_zero._proof_21 id, zpow_zero' := sign_type.comm_group_with_zero._proof_22, zpow_succ' := sign_type.comm_group_with_zero._proof_23, zpow_neg' := sign_type.comm_group_with_zero._proof_24, exists_pair_ne := sign_type.comm_group_with_zero._proof_25, inv_zero := sign_type.comm_group_with_zero._proof_26, mul_inv_cancel := sign_type.comm_group_with_zero._proof_27}
@[protected, instance]
Equations
@[protected, instance]
Equations

sign_type is equivalent to fin 3.

Equations
def sign_type.cast {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
sign_type → α

Turn a sign_type into zero, one, or minus one. This is a coercion instance, but note it is only a has_coe_t instance: see note [use has_coe_t].

Equations
@[protected, instance]
def sign_type.has_coe_t {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
Equations
@[simp]
theorem sign_type.cast_eq_coe {α : Type u_1} [has_zero α] [has_one α] [has_neg α] (a : sign_type) :
@[simp]
theorem sign_type.coe_zero {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
0 = 0
@[simp]
theorem sign_type.coe_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
1 = 1
@[simp]
theorem sign_type.coe_neg_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
-1 = -1
@[simp]
def sign {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :

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

Equations
theorem sign_apply {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :
sign a = ite (0 < a) 1 (ite (a < 0) (-1) 0)
@[simp]
theorem sign_zero {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :
@[simp]
theorem sign_pos {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : 0 < a) :
@[simp]
theorem sign_neg {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : a < 0) :
sign a = -1
@[simp]
theorem sign_eq_zero_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
sign a = 0 a = 0
theorem sign_ne_zero {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
sign a 0 a 0
def sign_hom {α : Type u_1} [linear_ordered_ring α] :

sign as a monoid_with_zero_hom 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 = sign (1 + i) * sign (1 - i) ≠ sign 2 = 1. (complex.ordered_comm_ring)

Equations