English
Let R be a division semiring. Then there exists a distributive action of the nonnegative rationals ℚ≥0 on R, i.e. a scalar multiplication by elements of ℚ≥0 that respects addition and the zero element: for all a in ℚ≥0 and x,y in R, a · 0 = 0 and a · (x + y) = a · x + a · y.
Русский
Пусть R — делимое полукольцо. Существует распределённое скалярное действие неотрицательных рациональных чисел ℚ≥0 на R: для всех a ∈ ℚ≥0 и x, y ∈ R выполняются a · 0 = 0 и a · (x + y) = a · x + a · y.
LaTeX
$$$\\forall a \\in \\mathbb{Q}_{\\ge 0}, \\forall x,y \\in R:\\ a \\cdot 0 = 0 \\land a \\cdot (x+y) = a \\cdot x + a \\cdot y$$$
Lean4
instance (priority := 100) instDistribSMul : DistribSMul ℚ≥0 R
where
smul_zero a := by rw [smul_def, mul_zero]
smul_add a x y := by rw [smul_def, smul_def, smul_def, mul_add]
