down_intCast

Mathlib.Algebra.Ring.ULift

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

English

For any R with an IntCast, and any integer n, down(n : ULift R) = n as an element of R.

Русский

Для любого R с intCast, и любого целого n, down(n : ULift R) = n в R.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem down_intCast [IntCast R] (n : ℤ) : down (n : ULift R) = n :=
  rfl

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

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

Разделы

Аффилиация

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