Galois Aut map one

theorem galoisAut_map_one (α i : ℕ) : galoisAut (powTwoCyclotomic (R := R) α) i 1 = 1 := by  have h2 : (0 : ℕ) < 2 ^ α := pow_pos (by norm_num) α  have hpos : 0 < (powTwoCyclotomic (R := R) α).φ.natDegree := by    rw [powTwoCyclotomic_natDegree]; exact h2  have hone : (1 : Rq (powTwoCyclotomic (R := R) α)).1 = (1 : CPolynomial R) := by    change (powTwoCyclotomic (R := R) α).reduce 1 = 1    refine CyclotomicModulus.reduce_eq_self_of_degree_lt _ ?_    rw [CompPoly.CPolynomial.toPoly_one, Polynomial.degree_one, powTwoCyclotomic_toPoly,      ← Polynomial.C_1, Polynomial.degree_X_pow_add_C h2 (1 : R)]    exact_mod_cast h2  have hcoeff : ∀ k,      (1 : Rq (powTwoCyclotomic (R := R) α)).1.coeff k = if k = 0 then (1 : R) else 0 :=    fun k => by rw [hone]; exact CompPoly.CPolynomial.coeff_one k  have hm : (monomial 0 (1 : R) : CPolynomial R) = 1 :=    CompPoly.CPolynomial.eq_iff_coeff.mpr fun j => by      rw [CompPoly.CPolynomial.coeff_monomial, CompPoly.CPolynomial.coeff_one]  unfold galoisAut  rw [Finset.sum_eq_single_of_mem 0 (Finset.mem_range.mpr hpos)        (fun k _ hk => by rw [hcoeff, if_neg hk, monomial_eq_zero]),      hcoeff, if_pos rfl, Nat.zero_mul, hm]  rfl