English
If K is GroupWithZero and there is a MulAction on each R i, then for r ≠ 0, r • S.pi t = S.pi (r • t) (via Units).
Русский
Если K — GroupWithZero и действует на каждый R_i, то при r ≠ 0 выполняется r • S.pi t = S.pi (r • t) (через единицы).
LaTeX
$$$\\forall r \\in K, r \\neq 0 \\Rightarrow r \\cdot S.\\pi t = S.\\pi (r \\cdot t).$$$
Lean4
theorem smul_pi₀ [GroupWithZero K] [∀ i, MulAction K (R i)] {r : K} (S : Set ι) (t : ∀ i, Set (R i)) (hr : r ≠ 0) :
r • S.pi t = S.pi (r • t) :=
smul_pi (Units.mk0 r hr) S t