down_natCast

Mathlib.Algebra.Ring.ULift

URI: https://scilib.ai/kg/mathlib#ULift.down_natCast

English

For any Type R with a NatCast, and any natural n, down(n : ULift R) = n.

Русский

Для любого типа R с нат.cast, и любого натурального n, down(n : ULift R) = n.

LaTeX

$$$\\mathrm{down}(n : \\mathrm{ULift} R) = (n : R)$$$

Lean4

@[simp, norm_cast]
theorem down_natCast [NatCast R] (n : ℕ) : down (n : ULift R) = n :=
  rfl

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

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

Разделы

Аффилиация

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