AnabelianGeometry.KummerTheory.exists_pow_eq_one_mul_or_inv_of_zpowers_pow_eq
The ambiguity in recovering a non-torsion generator from its powered cyclic subgroup is exactly inversion and multiplication by an n-th root of unity.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.KummerTheory
variable {G : Type*} [CommGroup G]Lean source · statement
theorem exists_pow_eq_one_mul_or_inv_of_zpowers_pow_eq
(n : ℕ+) (a b : G) (ha : ¬ IsOfFinOrder a)
(h : Subgroup.zpowers (a ^ (n : ℕ)) = Subgroup.zpowers (b ^ (n : ℕ))) :
∃ ζ : G, ζ ^ (n : ℕ) = 1 ∧ (b = ζ * a ∨ b = ζ * a⁻¹)