toFinset_factors

Mathlib.Data.Nat.PrimeFin

URI: https://scilib.ai/kg/mathlib#Nat.toFinset_factors

English

The finset of prime factors matches the toFinset image of the prime factors list.

Русский

Множество простых делителей совпадает с преобразованием списка делителей в Finset.

LaTeX

$$$n.\text{primeFactorsList}.toFinset = n.\text{primeFactors}$$$

Lean4

@[simp]
theorem toFinset_factors (n : ℕ) : n.primeFactorsList.toFinset = n.primeFactors :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru