cast_two

Mathlib.Data.Nat.Cast.Defs

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

English

For any R with NatCast, the cast of 2 equals 2 in R.

Русский

Для любого R с NatCast отображение двойки в R равно 2.

LaTeX

$$$ (2 : \mathbb{N})^{\uparrow} = 2 $$$

Lean4

theorem cast_two [NatCast R] : ((2 : ℕ) : R) = (2 : R) :=
  rfl

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

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

Разделы

Аффилиация

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