inl_mul_inl — Mathlib

English

Equality of left injections under multiplication: (inl r1) * (inl r2) = inl (r1 r2).

Русский

Равенство левым вложениям под умножением: inl(r1) * inl(r2) = inl(r1 r2).

LaTeX

$$$\mathrm{inl}(r_{1}) * \mathrm{inl}(r_{2}) = \mathrm{inl}(r_{1} r_{2})$$$

Lean4

theorem inl_mul_inl [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) :
    (inl r₁ * inl r₂ : tsze R M) = inl (r₁ * r₂) :=
  (inl_mul M r₁ r₂).symm

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