English
The finite set of monic irreducible factors of the minimal polynomial of θ modulo p, i.e., the factorization pattern of minpoly modulo p.
Русский
Построение конечного множества моник-неравных факторов минимального полинома θ по модулю p.
LaTeX
$$$\\text{monicFactorsMod} : \\mathrm{Finset}((\\mathbb{Z}/p\\mathbb{Z})[X]).$$$
Lean4
theorem ZModXQuotSpanEquivQuotSpan_mk_apply (hp : ¬p ∣ exponent θ) (Q : ℤ[X]) :
(ZModXQuotSpanEquivQuotSpan hp)
(Ideal.Quotient.mk (span {map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) (map (Int.castRingHom (ZMod p)) Q)) =
Ideal.Quotient.mk (span {(p : 𝓞 K)}) (aeval θ Q) :=
by
simp only [ZModXQuotSpanEquivQuotSpan, AlgEquiv.toRingEquiv_eq_coe, algebraMap_int_eq, RingEquiv.trans_apply,
AlgEquiv.coe_ringEquiv, quotientEquivAlgOfEq_mk, quotientEquiv_symm_apply, quotientMap_mk, RingHom.coe_coe,
mapEquiv_symm_apply, Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom]
exact
congr_arg (quotientEquivAlgOfEq ℤ (by simp [map_span])) <|
quotMapEquivQuotQuotMap_symm_apply (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral Q
