English
If M and M₂ are AddCommMonoid with modules over ℚ≥0, and F is a FunLike M → M₂ with AddMonoidHomClass, then for c ∈ ℚ≥0 and x ∈ M, f(c • x) = c • f(x).
Русский
Если M и M₂ — AddCommMonoid с модулями над ℚ≥0 и F — FunLike M → M₂, то для c ∈ ℚ≥0 и x ∈ M выполняется f(c • x) = c • f(x).
LaTeX
$$$f(c \\cdot x) = c \\cdot f(x)\\quad (c \\in \\mathbb{Q}_{\\ge 0}, x \\in M)$$$
Lean4
theorem map_nnrat_smul [AddCommMonoid M] [AddCommMonoid M₂] [_instM : Module ℚ≥0 M] [_instM₂ : Module ℚ≥0 M₂]
{F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ≥0) (x : M) : f (c • x) = c • f x :=
map_nnratCast_smul f ℚ≥0 ℚ≥0 c x
