English
For index set ι with decidable equality, a family M i with AddMonoid structures, and i, a, j in ι, the multiplicative version of Pi.mulSingle applied to i with ofAdd a at j equals the additive version of Pi.mulSingle.
Русский
Для множества индексов ι с разрешимой равенством, семейства M i с структурами AddMonoid и элементов i, a, j ∈ ι выполняется равенство между двумя версиями Pi.mulSingle.
LaTeX
$$$\forall {\iota} [\text{DecidableEq } ι] \{M : ι \to Type*\} \[(i : ι) \to AddMonoid (M i)] (i : ι) (a : M i) (j : ι),\n \mathrm{Pi.mulSingle} (M := λ i, \mathrm{Multiplicative} (M i)) i (\mathrm{ofAdd} a) j = \mathrm{ofAdd} (\mathrm Pi.single i a j)$$$
Lean4
theorem mulSingle_multiplicativeOfAdd_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*} [(i : ι) → AddMonoid (M i)] (i : ι)
(a : M i) (j : ι) : Pi.mulSingle (M := fun i ↦ Multiplicative (M i)) i (.ofAdd a) j = .ofAdd (Pi.single i a j) :=
by
rcases eq_or_ne j i with rfl | h
· simp only [mulSingle_eq_same, single_eq_same]
· simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single, zero_apply, ofAdd_zero]
