intCast_toProd

Mathlib.Analysis.CStarAlgebra.Multiplier

URI: https://scilib.ai/kg/mathlib#DoubleCentralizer.intCast_toProd

English

A third affirmation of natCast toProd coherence.

Русский

Третье утверждение когерентности natCast к toProd.

LaTeX

$$$ (n : 𝓜(𝕜, A)).toProd = n.cast.toProd$$$

Lean4

@[simp]
theorem intCast_toProd (n : ℤ) : (n : 𝓜(𝕜, A)).toProd = n :=
  rfl

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

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

Разделы

Аффилиация

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