instSMulCommClass — Mathlib

English

If the actions of R and S on V commute, then the induced actions commute on HahnSeries Γ V as well; i.e., SMulCommClass R S (HahnSeries Γ V).

Русский

Если действия R и S на V коммутируют, то соответствующие действия коммутируют и на HahnSeries Γ V: SMulCommClass R S (HahnSeries Γ V).

LaTeX

$$$\\text{SMulCommClass } R\\ S\\ (\\ HahnSeries \\;\\Gamma\\; V)$$$

Lean4

instance [SMulCommClass R S V] : SMulCommClass R S (HahnSeries Γ V) :=
  ⟨fun r s a => by
    ext
    simp [smul_comm]⟩

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