cast_zero

Mathlib.Data.Nat.Cast.Defs

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

English

If R is an additive monoid with one, the natural number zero casts to the zero element of R.

Русский

Пусть R — аддитивное моноид с единицей. Нуль из натуральных чисел отображается в 0 в R.

LaTeX

$$$ (0 : R) = 0 $$$

Lean4

@[simp, norm_cast]
theorem cast_zero : ((0 : ℕ) : R) = 0 :=
  AddMonoidWithOne.natCast_zero

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

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

Разделы

Аффилиация

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