English
For all i, if r acts on R i, then r · π(univ) t equals π(univ) (r · t).
Русский
Для всех i, если r действует на R_i, то r · π(univ) t = π(univ) (r · t).
LaTeX
$$$r \\cdot \\pi (\\mathrm{univ} : \\mathrm{Set} \\ \\i) t = \\pi (\\mathrm{univ} : \\mathrm{Set} \\ i) (r \\cdot t).$$$
Lean4
@[to_additive]
theorem smul_univ_pi [∀ i, SMul K (R i)] (r : K) (t : ∀ i, Set (R i)) :
r • pi (univ : Set ι) t = pi (univ : Set ι) (r • t) :=
piMap_image_univ_pi _ _