English
Under a factor orderIso, emultiplicity is preserved between m and n via the image of p.
Русский
При рассмотрении отображения между цепями делителей сохраняется эмпемтипичность между m и n через образ p.
LaTeX
$$emultiplicity p m = emultiplicity (RelIso.instFunLike.coe d ⟨p, ⋯⟩).val n$$
Lean4
theorem emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso {m p : Associates M} {n : Associates N}
(hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
emultiplicity p m = emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n :=
by
refine le_antisymm (emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso hp d) ?_
suffices
emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n ≤
emultiplicity (↑(d.symm (d ⟨p, dvd_of_mem_normalizedFactors hp⟩))) m
by
rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this
exact this
letI := Classical.decEq (Associates N)
simpa only [Subtype.coe_eta] using
emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso
(mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors hn hp d) d.symm
