English
For a list l of indices and corresponding elements, the product in the direct sum equals the product of the images under DirectSum.of, distributed along the list.
Русский
Для списка индексов l и соответствующих элементов произведение в прямой сумме равняется произведению образов через DirectSum.of, распределяя по списку.
LaTeX
$$$ (\text{List}.\text{dProd} \ f) \;:\; \text{List}.\text{map} (\text{of } A) \rhd \text{prod} = \text{of} A (\text{dProd} f) $$$
Lean4
theorem ofPow {i} (a : A i) (n : ℕ) : of _ i a ^ n = of _ (n • i) (GradedMonoid.GMonoid.gnpow _ a) := by
induction n with
| zero => exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
| succ n n_ih =>
rw [pow_succ, n_ih, of_mul_of]
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm
