inl_mul — Mathlib

English

Left injection preserves multiplication: inl(r1) * inl(r2) = inl(r1 r2) for monoid R with distributive actions.

Русский

Левое вложение сохраняет умножение: inl(r1) * inl(r2) = inl(r1 r2).

LaTeX

$$$(\mathrm{inl}(r_{1}) * \mathrm{inl}(r_{2}) : \mathrm{tsze}_{R} M) = \mathrm{inl}(r_{1} r_{2})$$$

Lean4

@[simp]
theorem inl_mul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) :
    (inl (r₁ * r₂) : tsze R M) = inl r₁ * inl r₂ :=
  ext rfl <| show (0 : M) = r₁ •> (0 : M) + (0 : M) <• r₂ by rw [smul_zero, zero_add, smul_zero]

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