mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors

English

If p is a member of the normalized factors of m, then the image of p under a factor order is a member of the normalized factors of n.

Русский

Если p принадлежит нормализованным факторизациям m, образ p как факторного порядка принадлежит нормализованным факторизациям n.

LaTeX

$$p ∈ normalizedFactors m → (d ⟨p, ⋯⟩) ∈ normalizedFactors n$$

Lean4

theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors {m p : Associates M} {n : Associates N}
    (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
    (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ∈ normalizedFactors n :=
  by
  obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd hn (map_prime_of_factor_orderIso hn hp d).irreducible
      (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop
  rw [associated_iff_eq] at hq'
  rwa [hq']

Похожие утверждения