cast_pred

Mathlib.Data.Int.Cast.Basic

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

← MathLib Explorer

English

If 0 < n, then the cast of (n − 1) equals n − 1 in any AddGroupWithOne R.

Русский

Пусть 0 < n. Тогда отображение (n − 1) в R равно n − 1.

LaTeX

$$$((n - 1) : R) = n - 1 \quad (n > 0)$$$

Lean4

@[simp, norm_cast]
theorem cast_pred : ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1
  | 0, h => by cases h
  | n + 1, _ => by rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]

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

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

Разделы

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

Аффилиация

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