Proper powers in free groups

Free generators and commutators of distinct generators are not proper powers. The latter is detected by the integer Heisenberg group: the commutator has central coordinate one.

theorem FreeGroup.isProperPower_of_sq {α : Type u_1} (a : α) : Group.IsProperPower (of a ^ 2)

The square of any free generator is a proper power.

theorem FreeGroup.exists_monoidHom_apply_eq_ofAdd_one {α : Type u_1} (a : α) : ∃ (f : FreeGroup α →* Multiplicative ℤ), f (of a) = Multiplicative.ofAdd 1

A coordinate homomorphism sending a chosen free generator to the generator of Multiplicative ℤ.

@[simp]

theorem FreeGroup.not_isProperPower_of {α : Type u_1} (a : α) : ¬Group.IsProperPower (of a)

A free generator is not a proper power.

theorem FreeGroup.natAbs_eq_one_of_of_eq_zpow {α : Type u_1} {a : α} {r : FreeGroup α} {m : ℤ} (h : of a = r ^ m) : m.natAbs = 1

If a generator of a free group is the m-th power of some element, then m = ±1.

theorem FreeGroup.not_isProperPower_commutator {α : Type u_1} {a b : α} (hab : a ≠ b) : ¬Group.IsProperPower ⁅of a, of b⁆

The commutator of two distinct free generators is not a proper power.