count_some — Mathlib

English

Count of a prime p inside a certain top-level factorization of a multiset s equals the count of the corresponding irreducible p in s.

Русский

Количество простого p внутри разложения множества s равно количеству соответствующего ирредуцируемого p в s.

LaTeX

$$$\text{count}_{p}(\mathrm{WithTop}.some\,s) = \mathrm{Multiset}.count\langle p,\, hp\rangle s$$$

Lean4

@[simp]
theorem count_some (hp : Irreducible p) (s : Multiset _) : count p (WithTop.some s) = s.count ⟨p, hp⟩ := by
  simp only [count, dif_pos hp, bcount]

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