mul_injections — Mathlib

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

Похожие утверждения