intCast_def

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.intCast_def

English

Integer casting in SkewMonoidAlgebra is given by singleton with 1 in G and the integer value in k.

Русский

Приведение к целым в SkewMonoidAlgebra задается единицей в G и целым значением коэффициента.

LaTeX

$$$$ (z : SkewMonoidAlgebra k G) = single (1 : G) (z : k) $$ for integers z$$

Lean4

theorem intCast_def (z : ℤ) : (z : SkewMonoidAlgebra k G) = single (1 : G) (z : k) := by cases z <;> simp

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

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

Разделы

Аффилиация

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