natCast_def

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

For every n ∈ ℕ, n in SkewMonoidAlgebra k G equals single(1_G) n.

Русский

Для каждого n ∈ ℕ, элемент n в SkewMonoidAlgebra k G равен single(1_G) n.

LaTeX

$$$\\forall n:\\\\mathbb{N},\\ (n:\\ SkewMonoidAlgebra\\ k\\ G) = \\mathrm{single}(1:G)(n:k)$$$

Lean4

theorem natCast_def (n : ℕ) : (n : SkewMonoidAlgebra k G) = single (1 : G) (n : k) := by induction n <;> simp_all

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

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

Разделы

Аффилиация

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