toEnd_intCast

Mathlib.Algebra.Ring.CentroidHom

URI: https://scilib.ai/kg/mathlib#CentroidHom.toEnd_intCast

English

The lemma that z.cast.toEnd equals z.cast for Int into End.

Русский

Лемма: z.cast.toEnd = z.cast для целых чисел в End.

LaTeX

$$$z.cast.toEnd = z.cast$$$

Lean4

@[simp, norm_cast]
theorem toEnd_intCast (z : ℤ) : (z : CentroidHom α).toEnd = ↑z :=
  rfl

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

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

Разделы

Аффилиация

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