cast_one

Mathlib.Data.Nat.Cast.Defs

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

English

For any R with AddMonoidWithOne, the cast of 1 is equal to 1 in R.

Русский

Для любого R с AddMonoidWithOne отображение единицы в R равно единице.

LaTeX

$$$ (1 : \mathbb{N}) \uparrow = 1 $$$

Lean4

@[simp, norm_cast]
theorem cast_one [AddMonoidWithOne R] : ((1 : ℕ) : R) = 1 := by rw [cast_succ, Nat.cast_zero, zero_add]

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

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

Разделы

Аффилиация

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