rat — Mathlib

English

For Monoid α, AddCommMonoid M, DistribMulAction α M, Module Rat M, the SMulCommClass Rat α M holds; i.e., Rat-scalars commute with α-actions.

Русский

Для α, M и Rat-структуры на M выполняется SMulCommClass Rat α M: рациональные скаляры коммутируют с α-действиями.

LaTeX

$$$\\text{SMulCommClass } \\mathrm{Rat} \\; \\alpha \\; M$$$

Lean4

instance rat [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] : SMulCommClass ℚ α M where
  smul_comm r x y := (map_rat_smul (DistribMulAction.toAddMonoidHom M x) r y).symm

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