SMulCommClass — Mathlib

English

The order of applying scalars and module actions can be swapped as in a commuting pair.

Русский

Порядок применения скаляра и действия модуля может быть поменян.

LaTeX

$$$\mathrm{SMulCommClass}\ R\ (\mathrm{HahnSeries}\; \Gamma\; R)\ (\mathrm{HahnModule}\; \Gamma'\; R\ V)$$$

Lean4

instance SMulCommClass [CommSemiring R] [Module R V] : SMulCommClass R (HahnSeries Γ R) (HahnModule Γ' R V) where
  smul_comm r x y := by rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]

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