single_smul₀ — Mathlib

English

Let g(i) be monoids with a MonoidWithZero structure and a DistribMulAction by f(i) on g(i). Then single i (r • x) = single i r • single i x.

Русский

Пусть g(i) — монойды с нулём; действует распределённо от f(i) на g(i). Тогда single i (r • x) = single i r • single i x.

LaTeX

$$$\forall i, \; single_i (r \cdot x) = single_i r \cdot single_i x$$$

Lean4

theorem single_smul₀ {g : I → Type*} [∀ i, MonoidWithZero (f i)] [∀ i, AddMonoid (g i)]
    [∀ i, DistribMulAction (f i) (g i)] [DecidableEq I] (i : I) (r : f i) (x : g i) :
    single i (r • x) = single i r • single i x :=
  single_op₂ (fun i : I => ((· • ·) : f i → g i → g i)) (fun _ => smul_zero _) _ _ _

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