Fixed Subring is Field

theorem fixedSubring_isField (hq5 : q % 8 = 5) {α κ : ℕ} (hα : 1 ≤ α) :    IsField (fixedSubring (R := ZMod q) α (2 ^ κ)) := by  have hconjF := conjFixedSubring_isField q hq5 hα  have hle := fixedSubring_le_conjFixedSubring (R := ZMod q) α (2 ^ κ)  -- Derive `Nontrivial`/`NoZeroDivisors` on `R_q^{σ_{-1}}` from the `IsField` *Prop* directly,  -- avoiding the instance diamond that `IsField.toField` would create on the subring carrier.  haveI : Nontrivial (conjFixedSubring (R := ZMod q) α) := ⟨hconjF.exists_pair_ne⟩  haveI : NoZeroDivisors (conjFixedSubring (R := ZMod q) α) := by    refine ⟨fun {a b} hab => ?_⟩    by_cases ha : a = 0    · exact Or.inl ha    · obtain ⟨a', haa'⟩ := hconjF.mul_inv_cancel ha      refine Or.inr ?_      have h0 : a' * (a * b) = 0 := by rw [hab, mul_zero]      rwa [← mul_assoc, mul_comm a' a, haa', one_mul] at h0  -- Pull the domain structure back along the injective inclusion `R_q^H ↪ R_q^{σ_{-1}}`.  haveI : Nontrivial (fixedSubring (R := ZMod q) α (2 ^ κ)) :=    (Subring.inclusion hle).domain_nontrivial  haveI : NoZeroDivisors (fixedSubring (R := ZMod q) α (2 ^ κ)) :=    Function.Injective.noZeroDivisors (Subring.inclusion hle) (Subring.inclusion_injective hle)      (Subring.inclusion hle).map_zero (fun x y => (Subring.inclusion hle).map_mul x y)  haveI : IsDomain (fixedSubring (R := ZMod q) α (2 ^ κ)) := NoZeroDivisors.to_isDomain _  exact Finite.isField_of_domain _