dvd_of_mem_normalizedFactors — Mathlib

English

If every factor of a given r is equal to a fixed p, then r is associated to a power of p.

Русский

Если все множители r равны фиксированному p (до ассоциаций), то r ассоциировано с некоторой степенью p.

LaTeX

$$(∀ {m}, m ∈ normalizedFactors r → m = p) ∧ r ≠ 0 → ∃ i ∈ ℕ, Associated(p^i, r)$$

Lean4

theorem dvd_of_mem_normalizedFactors {a p : α} (H : p ∈ normalizedFactors a) : p ∣ a :=
  by
  by_cases hcases : a = 0
  · rw [hcases]
    exact dvd_zero p
  · exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

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