mulSingle_apply_commute — Mathlib

English

If x is a function I → f i, then for any i, j, the elements mulSingle i (x i) and mulSingle j (x j) commute.

Русский

Пусть x : ∀ i, f i. Тогда для любых i, j элементы mulSingle i (x i) и mulSingle j (x j) commute.

LaTeX

$$$\mathrm{Commute}(\mathrm{mulSingle}_i(x_i), \mathrm{mulSingle}_j(x_j))$$$

Lean4

/-- The injection into a pi group with the same values commutes. -/
@[to_additive /-- The injection into an additive pi group with the same values commutes. -/
    ]
theorem mulSingle_apply_commute [∀ i, MulOneClass <| f i] (x : ∀ i, f i) (i j : I) :
    Commute (mulSingle i (x i)) (mulSingle j (x j)) :=
  by
  obtain rfl | hij := Decidable.eq_or_ne i j
  · rfl
  · exact Pi.mulSingle_commute hij _ _

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