sigmaUncurry_smul — Mathlib

English

There is a compatibility of sigma-uncurry with scalar action: sigmaUncurry (r • f) = r • sigmaUncurry f for r in a monoid.

Русский

Совместимость σ-uncurry с действием скаляра: sigmaUncurry (r • f) = r • sigmaUncurry f, где r принадлежит моноиду.

LaTeX

$$$\sigma\text{-Uncurry}(r \cdot f) = r \cdot \sigma\text{-Uncurry}(f)$$$

Lean4

@[simp]
theorem sigmaUncurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ)
    (f : Π₀ (i) (j), δ i j) : sigmaUncurry (r • f) = r • sigmaUncurry f :=
  DFunLike.coe_injective rfl

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