cast_four

Mathlib.Data.Nat.Cast.Defs

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

English

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

Русский

Для любого R с NatCast отображение четырех в R равно 4.

LaTeX

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

Lean4

theorem cast_four [NatCast R] : ((4 : ℕ) : R) = (4 : R) :=
  rfl

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

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

Разделы

Аффилиация

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