le_of_mem_primeFactors

Mathlib.Data.Nat.PrimeFin

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

English

If p ∈ primeFactors(n), then p ≤ n.

Русский

Если p ∈ primeFactors(n), то p ≤ n.

LaTeX

$$$p \in n.\text{primeFactors} \Rightarrow p \le n$$$

Lean4

theorem le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
  le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt <| dvd_of_mem_primeFactors h

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

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

Разделы

Аффилиация

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