normalizedFactors_eq_of_dvd — Mathlib

English

If p, q ∈ normalizedFactors a and p ∣ q, then p = q.

Русский

Если p, q ∈ normalizedFactors a и p делит q, то p = q.

LaTeX

$$p ∈ normalizedFactors a ∧ q ∈ normalizedFactors a ∧ p ∣ q → p = q$$

Lean4

theorem normalizedFactors_eq_of_dvd (a : α) : ∀ᵉ (p ∈ normalizedFactors a) (q ∈ normalizedFactors a), p ∣ q → p = q :=
  by
  intro p hp q hq hdvd
  convert
      normalize_eq_normalize hdvd
        ((prime_of_normalized_factor _ hp).irreducible.dvd_symm (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
    apply (normalize_normalized_factor _ ‹_›).symm

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