inr_mul_inl — Mathlib

English

Similarly, a · inl(r) = inr(r • a) for a ∈ A, r ∈ R.

Русский

Аналогично: a · inl(r) = inr(r • a).

LaTeX

$$$a \cdot \mathrm{inl}(r) = \mathrm{inr}(r \cdot a).$$$

Lean4

theorem inr_mul_inl [MulZeroClass R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r : R) (a : A) :
    a * (inl r : Unitization R A) = ↑(r • a) :=
  ext (zero_mul r) <| show (0 : R) • (0 : A) + r • a + a * 0 = r • a by rw [smul_zero, zero_add, mul_zero, add_zero]

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