divisors_sq

Mathlib.Data.Finset.NatDivisors

URI: https://scilib.ai/kg/mathlib#Nat.Prime.divisors_sq

English

If p is a prime, the divisors of p^2 are exactly {1, p, p^2}.

Русский

Пусть p — простое число. Делители числа p^2 равны {1, p, p^2}.

LaTeX

$$$p\\text{ простое} \\implies (p^2).\\operatorname{divisors} = \\{1, p, p^2\\}$.$$

Lean4

theorem divisors_sq {p : ℕ} (hp : p.Prime) : (p ^ 2).divisors = {p ^ 2, p, 1} := by
  simp [divisors_prime_pow hp, range_add_one]

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

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

Разделы

Аффилиация

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