inl_mul — Mathlib

English

The map inl: R → Unitization(R, A) preserves multiplication; i.e., inl(r1 r2) = inl(r1) · inl(r2).

Русский

Отображение inl: R → Unitization(R, A) сохраняет умножение: inl(r1 r2) = inl(r1) · inl(r2).

LaTeX

$$$\mathrm{inl}(r_1 r_2) = \mathrm{inl}(r_1) \cdot \mathrm{inl}(r_2).$$$

Lean4

@[simp]
theorem inl_mul [Mul R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r₁ r₂ : R) :
    (inl (r₁ * r₂) : Unitization R A) = inl r₁ * inl r₂ :=
  ext rfl <| show (0 : A) = r₁ • (0 : A) + r₂ • (0 : A) + 0 * 0 by simp only [smul_zero, add_zero, mul_zero]

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