Equality of signs

The group ℤˣ = {±1} has exponent two, so two signs are equal exactly when their product is 1. This is the form in which an equality of two products of Hilbert symbols is checked, by expanding both sides into one common product of symbols.

Main results

• Int.units_eq_iff_mul_eq_one: u = v ↔ u * v = 1 for signs u v : ℤˣ.
• Int.units_eq_iff_eq_of_mul_eq_mul: if u * v = u' * v' then u = v ↔ u' = v'.

theorem Int.units_eq_iff_mul_eq_one (u v : ℤˣ) : u = v ↔ u * v = 1

Two signs are equal exactly when their product is 1.

theorem Int.units_eq_iff_eq_of_mul_eq_mul {u v u' v' : ℤˣ} (h : u * v = u' * v') : u = v ↔ u' = v'

Two pairs of signs with the same product agree in the same cases: if u * v = u' * v' then u = v exactly when u' = v'.