English
Multiplication inside the free product corresponds to pointwise multiplication inside the same A_i via the injections.
Русский
Умножение внутри свободного произведения соответствует покомпонентному умножению внутри того же A_i через инъекции.
LaTeX
$$$\iota'_R A (DirectSum.lof R I A i a_1) * \iota'_R A (DirectSum.lof R I A i a_2) = \iota'_R A (DirectSum.lof R I A i (a_1 a_2))$$$
Lean4
/-- Multiplication in the free product of the injections of any two `aᵢ aᵢ': A i` for
the same `i` is just the injection of multiplication `aᵢ * aᵢ'` in `A i`. -/
theorem mul_injections (a₁ a₂ : A i) :
ι' R A (DirectSum.lof R I A i a₁) * ι' R A (DirectSum.lof R I A i a₂) = ι' R A (DirectSum.lof R I A i (a₁ * a₂)) :=
by
convert RingQuot.mkAlgHom_rel R <| rel.prod
simp