factorization_one_right

Mathlib.Data.Nat.Factorization.Defs

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

English

For every n, the exponent of 1 in n’s factorization is 0.

Русский

Для каждого n показатель степени 1 в факторизации n равен 0.

LaTeX

$$$\\operatorname{factorization}(n)(1) = 0$$$

Lean4

@[simp]
theorem factorization_one_right (n : ℕ) : n.factorization 1 = 0 :=
  factorization_eq_zero_of_not_prime _ not_prime_one

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

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

Разделы

Аффилиация

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