factorization_zero_right

Mathlib.Data.Nat.Factorization.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem factorization_zero_right (n : ℕ) : n.factorization 0 = 0 :=
  factorization_eq_zero_of_non_prime _ not_prime_zero

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

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

Разделы

Аффилиация

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