factorization_zero — Mathlib

English

Let n be a natural number. The prime-power decomposition of 0 is the zero vector; equivalently, the factorization of 0 is 0.

Русский

Пусть n — натуральное число. Разложение по степеням простых числа для 0 является нулевым вектором; эквивалентно: 0 = факторизация(0).

LaTeX

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

Lean4

@[simp]
theorem factorization_zero : factorization 0 = 0 := by ext; simp [factorization]

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