pred_pos

Mathlib.Data.Nat.Prime.Basic

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

English

If p is prime, then pred(p) is positive.

Русский

Если p простое, то pred(p) положительно.

LaTeX

$$$$ \text{Prime}(p) \Rightarrow 0 < p - 1. $$$$

Lean4

theorem pred_pos {p : ℕ} (pp : Prime p) : 0 < pred p :=
  lt_pred_iff.2 pp.one_lt

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

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

Разделы

Аффилиация

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