inl_mul_inr — Mathlib

English

Cross terms satisfy: inl(r) · inr(a) = inr(r • a).

Русский

Смешанные пары удовлетворяют: inl(r) · inr(a) = inr(r • a).

LaTeX

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

Lean4

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

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