prime_pow_le_iff_le_bcount — Mathlib

English

Let m be a nonzero Associate, p irreducible. Then p^k ≤ m iff k ≤ the bcount of ⟨p,h⟩ in m.factors.

Русский

Пусть m ≠ 0. Тогда p^k ≤ m, если и только если k ≤ количество повторов p в m.factors.

LaTeX

$$$$m \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow p^k \\le m \\iff k \\le \\mathrm{bcount}\\langle p,hp\\rangle m.factors.$$$$

Lean4

theorem prime_pow_le_iff_le_bcount [DecidableEq (Associates α)] {m p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p)
    {k : ℕ} : p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors :=
  by
  rcases Associates.exists_non_zero_rep h₁ with ⟨m, hm, rfl⟩
  have := nontrivial_of_ne _ _ hm
  rw [bcount.eq_def, factors_mk, Multiset.le_count_iff_replicate_le, ← factors_le, factors_prime_pow, factors_mk,
      WithTop.coe_le_coe] <;>
    assumption

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