factorization_eq_count — Mathlib

English

For any n and p, the value of factorization(n) at p equals the number of occurrences of p in normalizedFactors(n).

Русский

Для любых n и p значение factorization(n) на p равно числу вхождений p в normalizedFactors(n).

LaTeX

$$$\\forall n\\,p,\\ n\\text{ и }p:\\ factorization(n)(p) = \\operatorname{Multiset}.count(p, \\operatorname{normalizedFactors}(n))$$$

Lean4

theorem factorization_eq_count {n p : α} : factorization n p = Multiset.count p (normalizedFactors n) := by
  simp [factorization]

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