nnrat — Mathlib

English

For Monoid α, AddCommMonoid M with DistribMulAction α M and Module ℚ≥0 M, the SMulCommClass ℚ≥0 α M holds, i.e., ℚ≥0-scalar actions commute with α-actions on M.

Русский

Для моноида α и M с DistribMulAction и модулем ℚ≥0 над M выполняется SMulCommClass ℚ≥0 α M: скаляры ℚ≥0 коммутируют с действием α на M.

LaTeX

$$$\\text{SMulCommClass } \\mathbb{Q}_{\\ge 0} \\; \\alpha \\; M$$$

Lean4

instance nnrat [Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] : SMulCommClass ℚ≥0 α M where
  smul_comm r x y := (map_nnrat_smul (DistribMulAction.toAddMonoidHom M x) r y).symm

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