coe_nsmul

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithBot.coe_nsmul

English

A simp/norm_cast variant of coe_nsmul.

Русский

Вариант simp/norm_cast для coe_nsmul.

LaTeX

$$$$ \\text{[simp, norm_cast] }\\forall a \\in \\alpha, \\forall n \\in \\mathbb{N},\\ ↑(n \\cdot a) = n \\cdot (a \\uparrow). $$$$

Lean4

@[simp, norm_cast]
theorem coe_nsmul (a : α) (n : ℕ) : ↑(n • a) = n • (a : WithBot α) :=
  (addHom : α →+ WithBot α).map_nsmul _ _

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

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

Разделы

Аффилиация

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