English
Let R be a division ring. Then there is a distributive action of the rational numbers on R, i.e. a ℚ-action on R that preserves zero and addition: a · 0 = 0 and a · (x + y) = a · x + a · y for all a ∈ ℚ and x,y ∈ R.
Русский
Пусть R — делимое кольцо. Существует распределённое скалярное действие рациональных чисел на R: для всех a ∈ ℚ и x,y ∈ R выполняются a · 0 = 0 и a · (x + y) = a · x + a · y.
LaTeX
$$$\\forall a \\in \\mathbb{Q}, \\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 ℚ 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]
