sub_eq_psub

Mathlib.Data.Nat.PSub

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

← MathLib Explorer

English

For all m,n, m - n equals (psub(m,n)).getD 0.

Русский

Для всех m,n, m - n = (psub(m,n)).getD 0.

LaTeX

$$$$ \forall m,n:\mathbb{N}, \ m - n = (psub(m,n)).getD(0). $$$$

Lean4

theorem sub_eq_psub (m : ℕ) : ∀ n, m - n = (psub m n).getD 0
  | 0 => rfl
  | n + 1 => (pred_eq_ppred (m - n)).trans <| by rw [sub_eq_psub m n, psub]; cases psub m n <;> rfl

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

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

Разделы

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

Аффилиация

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