Nonempty unramified Extension alghom of dvd f

theorem nonempty_unramifiedExtension_alghom_of_dvd_f (n : ℕ) (hn : n ∣ f K L) :    Nonempty (UnramifiedExtension K n →ₐ[K] L) := by  have hf0 := NeZero.mk (f_pos K L).ne'  have hn0 := NeZero.mk <| ne_zero_of_dvd_ne_zero hf0.out hn  have h₁ := Nat.pow_sub_one_dvd_pow_sub_one (Nat.card 𝓀[K]) hn  obtain ⟨ζ, hζ⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot    (UnramifiedExtension K n) (Nat.card 𝓀[K] ^ n - 1)  have h₂ := pos_of_ne_zero <| card_pow_sub_one_in_nat_ne_zero 𝓀[K] hn0.out  have h₃ := pos_of_ne_zero <| card_pow_sub_one_in_nat_ne_zero 𝓀[K] hf0.out  refine IntermediateField.nonempty_algHom_of_adjoin_splits    (forall_eq.mpr ⟨.of_pow h₂ <| hζ.1 ▸ isIntegral_one,      .of_dvd (g := X ^ (Nat.card 𝓀[K] ^ n - 1) - C 1) ?_        (X_pow_sub_C_ne_zero h₂ _) ?_⟩)    (intermediateFieldTop_eq_adjoin_primitive_root K _ hζ).symm  · rw [f_spec'] at h₁ h₃    have := NeZero.mk h₃.ne'    have := HasEnoughRootsOfUnity.of_dvd L h₁    obtain ⟨ζ', hζ'⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot L (Nat.card 𝓀[K] ^ n - 1)    simpa [Splits] using X_pow_sub_one_splits hζ'  · conv_rhs => exact show _ = map (algebraMap K L) (X ^ (Nat.card 𝓀[K] ^ n - 1) - C 1) by simp    rw [map_dvd_map', minpoly.dvd_iff]    simp [hζ.1]