normalizedFactors_irreducible — Mathlib

English

For irreducible a, normalizedFactors a equals the singleton {normalize a}.

Русский

Для неразложимого a нормализованные факторы a равны единственному элементу {normalize a}.

LaTeX

$$normalizedFactors(a) = {normalize a}$$

Lean4

theorem normalizedFactors_irreducible {a : α} (ha : Irreducible a) : normalizedFactors a = {normalize a} :=
  by
  obtain ⟨p, a_assoc, hp⟩ :=
    prime_factors_irreducible ha ⟨prime_of_normalized_factor, prod_normalizedFactors ha.ne_zero⟩
  have p_mem : p ∈ normalizedFactors a := by
    rw [hp]
    exact Multiset.mem_singleton_self _
  convert hp
  rwa [← normalize_normalized_factor p p_mem, normalize_eq_normalize_iff, dvd_dvd_iff_associated]

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