cast_three

Mathlib.Data.Nat.Cast.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem cast_three [NatCast R] : ((3 : ℕ) : R) = (3 : R) :=
  rfl

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

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

Разделы

Аффилиация

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