succ_pred_prime

Mathlib.Data.Nat.Prime.Basic

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

English

For a prime p, succ(pred(p)) = p.

Русский

Для простого p последовательность succ(pred(p)) равна p.

LaTeX

$$$$ \text{Prime}(p) \Rightarrow \operatorname{succ}(\operatorname{pred}(p)) = p. $$$$

Lean4

theorem succ_pred_prime {p : ℕ} (pp : Prime p) : succ (pred p) = p :=
  succ_pred_eq_of_pos pp.pos

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

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

Разделы

Аффилиация

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