primeFactors — Mathlib

English

The finite set of prime factors of an element in a unique factorization monoid.

Русский

Конечное множество простых делителей элемента в уникальном факторизационном моноиде.

LaTeX

$$$$ \text{primeFactors}(a) = \text{finite set of primes dividing } a. $$$$

Lean4

/-- The finite set of prime factors of an element in a unique factorization monoid. -/
def primeFactors (a : M) : Finset M :=
  (normalizedFactors a).toFinset

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