one_smul'

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnModule.one_smul'

← MathLib Explorer

English

Zero acts as the zero scalar: 0 • x = 0.

Русский

Нулевой скаляр действует как ноль: 0 • x = 0.

LaTeX

$$$0 \\cdot x = 0$$$

Lean4

@[simp]
theorem one_smul' {Γ} [AddCommMonoid Γ] [PartialOrder Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [MonoidWithZero R]
    [MulActionWithZero R V] {x : HahnModule Γ' R V} : (1 : HahnSeries Γ R) • x = x :=
  by
  ext g
  exact coeff_single_zero_smul.trans (one_smul R (x.coeff g))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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