English
For index ι with decidable equality and Monoid structure on each M i, Pi.single ofMul maps to the additive Pi.single in the expected way.
Русский
Для индексов ι с разрешимой равенством и моноидной структурой на каждом M i, Pi.single (Additive) соответствует ожидаемому выражению.
LaTeX
$$$\forall {\iota} [\text{DecidableEq } ι] {M : ι \to Type*} [(i : ι) \to Monoid (M i)] (i : ι) (a : M i) (j : ι),\n \mathrm Pi.single (M := \lambda i \mapsto Additive (M i)) i (.ofMul a) j = .ofMul (\mathrm Pi.mulSingle i a j)$$$
Lean4
theorem single_additiveOfMul_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*} [(i : ι) → Monoid (M i)] (i : ι) (a : M i)
(j : ι) : Pi.single (M := fun i ↦ Additive (M i)) i (.ofMul a) j = .ofMul (Pi.mulSingle i a j) :=
by
rcases eq_or_ne j i with rfl | h
· simp only [mulSingle_eq_same, single_eq_same]
· simp only [single, ne_eq, h, not_false_eq_true, Function.update_of_ne, zero_apply, mulSingle, one_apply, ofMul_one]
