English
If hp is a membership of p in normalizedFactors m, then the image of p under a factor orderIso belongs to normalizedFactors n.
Русский
Если hp — принадлежность p нормализованной факторизации m, то образ p под факторного порядка принадлежит нормализованным факторам n.
LaTeX
$$mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors hn hp d$$
Lean4
theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {m p : M} {n : N} (hm : m ≠ 0) (hn : n ≠ 0)
(hp : p ∈ normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
(hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ (l' : M)) :
↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩) ∈ normalizedFactors n :=
by
suffices
Prime
(d
⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
simp [dvd_of_mem_normalizedFactors hp]⟩ :
N)
by
simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
associatesEquivOfUniqueUnits_symm_apply] at this
obtain ⟨q, hq, hq'⟩ :=
exists_mem_normalizedFactors_of_dvd hn this.irreducible
(d ⟨p, by apply dvd_of_mem_normalizedFactors; convert hp⟩).prop
rwa [associated_iff_eq.mp hq']
have :
Associates.mk
(d
⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
associatesEquivOfUniqueUnits_symm_apply]⟩ :
N) =
↑(mkFactorOrderIsoOfFactorDvdEquiv hd
⟨associatesEquivOfUniqueUnits.symm p,
by
simp only [associatesEquivOfUniqueUnits_symm_apply]
exact mk_dvd_mk.mpr (dvd_of_mem_normalizedFactors hp)⟩) :=
by rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
rw [← Associates.prime_mk, this]
letI := Classical.decEq (Associates M)
refine map_prime_of_factor_orderIso (mk_ne_zero.mpr hn) ?_ _
obtain ⟨q, hq, hq'⟩ :=
exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
(prime_mk.mpr (prime_of_normalized_factor p (by convert hp))).irreducible
(mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
simpa only [associated_iff_eq.mp hq', associatesEquivOfUniqueUnits_symm_apply] using hq
