smul_univ_pi — Mathlib

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 _ _

Похожие утверждения