∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ}
  [inst_2 : Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ) (Q : Polynomial ℤ),
  (RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp)
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (Polynomial.map (Int.castRingHom (ZMod p)) Q)) =
    (Ideal.Quotient.mk (Ideal.span {↑p})) ((Polynomial.aeval θ) Q)