Sign factors of integers

The factor if x < 0 then -1 else 1 is the sign of a nonzero integer x, and its variant if p ∧ x < 0 then -1 else 1, which switches the sign on only under a side condition p, is multiplicative in x over nonzero factors. Such factors occur in the Kronecker symbol, whose value at the denominator -1 is the sign factor of the numerator.

Main statements

• Int.ite_lt_zero_eq_sign: for x ≠ 0, (if x < 0 then -1 else 1) = x.sign.
• Int.ite_and_mul_lt_zero: the factor if p ∧ x < 0 then -1 else 1 is multiplicative in x over nonzero factors.
• Int.sign_sub_mul_add_sign: for 0 ≤ a < M, the signs of a - m M and m cancel, except at m = 0.

theorem Int.ite_lt_zero_eq_sign {x : ℤ} (hx : x ≠ 0) : (if x < 0 then -1 else 1) = x.sign

For x ≠ 0, the sign factor if x < 0 then -1 else 1 is the sign of x.

theorem Int.ite_and_mul_lt_zero {p : Prop} [Decidable p] {x y : ℤ} (hx : x ≠ 0) (hy : y ≠ 0) : (if p ∧ x * y < 0 then -1 else 1) = (if p ∧ x < 0 then -1 else 1) * if p ∧ y < 0 then -1 else 1

The sign factor if p ∧ x < 0 then -1 else 1 is multiplicative in x over nonzero factors.

theorem Int.sign_sub_mul_add_sign {a M : ℤ} (ha₀ : 0 ≤ a) (ha : a < M) (m : ℤ) : (a - m * M).sign + m.sign = if m = 0 ∧ a ≠ 0 then 1 else 0

For 0 ≤ a < M, the signs of a - m M and of m cancel, except at m = 0, where their sum is the sign of a.