Xpow nat Degree

theorem Xpow_natDegree (α : ℕ) : Xpow (powTwoCyclotomic (R := R) α) (2 ^ α) = -1 := by  apply Rq.toQuotient_injective (powTwoCyclotomic α)  have hmem : (Polynomial.X ^ 2 ^ α + 1 : Polynomial R)      ∈ (powTwoCyclotomic (R := R) α).modIdeal := by    rw [modIdeal, powTwoCyclotomic_toPoly]; exact Ideal.mem_span_singleton_self _  have hzero : Ideal.Quotient.mk (powTwoCyclotomic (R := R) α).modIdeal      (Polynomial.X ^ 2 ^ α + 1) = 0 := Ideal.Quotient.eq_zero_iff_mem.mpr hmem  rw [map_add, map_one] at hzero  have hneg : Rq.toQuotient (powTwoCyclotomic (R := R) α) (-1) = -1 := by    have h := map_neg (Rq.toQuotientHom (powTwoCyclotomic (R := R) α)) 1    rw [map_one] at h    exact h  rw [Xpow_toQuotient, hneg]  exact eq_neg_of_add_eq_zero_left hzero