1 + a * b is a unit exactly when 1 + b * a is

In a ring, possibly noncommutative, the two products a * b and b * a are generally unrelated, but 1 + a * b and 1 + b * a are invertible together. This is the elementwise shadow of the fact that a * b and b * a have the same spectrum away from 0, and it is the mechanism behind the left-right symmetry of the Jacobson radical.

Mathlib records the spectral statement as spectrum.unit_mem_mul_comm. The elementwise form is that statement for the base ring ℤ, read at the unit 1, and that is how it is obtained here.

Main results

• TauCeti.isUnit_one_sub_mul_comm: IsUnit (1 - a * b) ↔ IsUnit (1 - b * a).
• TauCeti.isUnit_one_add_mul_comm: IsUnit (1 + a * b) ↔ IsUnit (1 + b * a).

theorem TauCeti.isUnit_one_sub_mul_comm {R : Type u_1} [Ring R] {a b : R} : IsUnit (1 - a * b) ↔ IsUnit (1 - b * a)

1 - a * b is a unit exactly when 1 - b * a is.

This is spectrum.unit_mem_mul_comm over the base ring ℤ, at the unit 1.

theorem TauCeti.isUnit_one_add_mul_comm {R : Type u_1} [Ring R] {a b : R} : IsUnit (1 + a * b) ↔ IsUnit (1 + b * a)

1 + a * b is a unit exactly when 1 + b * a is.