English
In the pi group, injections at distinct indices commute: if i ≠ j and x ∈ f i, y ∈ f j, then mulSingle i x and mulSingle j y commute.
Русский
В пи-группе инъекции с разных индексов взаимно приводят к коммутированию: если i ≠ j и x ∈ f i, y ∈ f j, то mulSingle i x и mulSingle j y commute.
LaTeX
$$$\forall i \neq j, \forall x \in f_i, \forall y \in f_j,\; \mathrm{Commute}(\mathrm{mulSingle}_i x, \mathrm{mulSingle}_j y)$$$
Lean4
/-- The injection into a pi group at different indices commutes.
For injections of commuting elements at the same index, see `Commute.map` -/
@[to_additive /-- The injection into an additive pi group at different indices commutes.
For injections of commuting elements at the same index, see `AddCommute.map` -/
]
theorem mulSingle_commute [∀ i, MulOneClass <| f i] :
Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y) :=
by
intro i j hij x y; ext k
by_cases h1 : i = k
· subst h1
simp [hij]
simp_all
