IsPrimitiveRoot.autToPow_injective

theorem IsPrimitiveRoot.autToPow_injective : ∀ {n : ℕ+} (K : Type u_1) [inst : Field K] {L : Type u_2} {μ : L} [inst_1 : CommRing L] [inst_2 : IsDomain L] (hμ : IsPrimitiveRoot μ ↑n) [inst_3 : Algebra K L] [inst_4 : IsCyclotomicExtension {n} K L], Function.Injective ⇑(IsPrimitiveRoot.autToPow K hμ)

The theorem `IsPrimitiveRoot.autToPow_injective` states that for any positive natural number `n`, any field `K`, any commutative ring `L` that is a domain, and any `μ` in `L` that is a primitive `n`th root of unity, the function `IsPrimitiveRoot.autToPow` is injective when it's considered over a cyclotomic field extension. This means that if two automorphisms are mapped to the same output by `IsPrimitiveRoot.autToPow`, then these two automorphisms were actually the same to begin with. In other words, `IsPrimitiveRoot.autToPow` uniquely identifies every automorphism.

More concisely: Given a positive natural number `n`, a field `K`, a commutative domain `L`, and a primitive `n`th root of unity `μ` in `L`, the function `IsPrimitiveRoot.autToPow` from automorphisms of `K` to `L⊥(X^n - 1)` is injective.