Shared inverse-commutator criteria for the Borisov and host constructions.

theorem Undecidability.CommutatorLemmas.inverse_commutator_eq_one_iff_commute {G : Type u_1} [Group G] (a b : G) : a⁻¹ * b⁻¹ * a * b = 1 ↔ Commute a b

The inverse-convention commutator is trivial exactly when its entries commute.

theorem Undecidability.CommutatorLemmas.inverse_commutator_eq_one_iff_mul_eq_mul {G : Type u_1} [Group G] (a b : G) : a⁻¹ * b⁻¹ * a * b = 1 ↔ a * b = b * a

The inverse-convention commutator criterion expressed as equality of products.