mulSingle_comp_equiv — Mathlib

English

The composition with an equiv interchanges with a single-index injection: Pi.mulSingle i x ∘ σ = Pi.mulSingle (σ^{-1} i) x.

Русский

Композиция с эквивалентом меняет место вставки: Pi.mulSingle i x ∘ σ = Pi.mulSingle (σ^{-1} i) x.

LaTeX

$$$\Pi.mulSingle i x \circ \sigma = \Pi.mulSingle (\sigma^{-1} i) x$$$

Lean4

@[to_additive]
theorem mulSingle_comp_equiv {m n : Type*} [DecidableEq n] [DecidableEq m] [One α] (σ : n ≃ m) (i : m) (x : α) :
    Pi.mulSingle i x ∘ σ = Pi.mulSingle (σ.symm i) x := by
  ext x
  aesop (add simp Pi.mulSingle_apply)

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