minFac_prime_iff

Mathlib.Data.Nat.Prime.Defs

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

← MathLib Explorer

English

minFac(p) is prime iff p ≠ 1.

Русский

minFac(p) простое тогда и только тогда, когда p ≠ 1.

LaTeX

$$$\\\\operatorname{Prime}(\minFac(p)) \iff p \neq 1.$$$

Lean4

@[simp]
theorem minFac_prime_iff {n : ℕ} : Prime (minFac n) ↔ n ≠ 1 :=
  by
  refine ⟨?_, minFac_prime⟩
  rintro h rfl
  simp only [minFac_one, not_prime_one] at h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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