inr_mul_inr — Mathlib

English

Product of two inr is zero: inr(m1) * inr(m2) = 0.

Русский

Произведение двух inr равно нулю: inr(m1) * inr(m2) = 0.

LaTeX

$$$(\mathrm{inr}(m_{1}) * \mathrm{inr}(m_{2}) : \mathrm{tsze}_{R} M) = 0$$$

Lean4

@[simp]
theorem inr_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) :
    (inr m₁ * inr m₂ : tsze R M) = 0 :=
  ext (mul_zero _) <| show (0 : R) •> m₂ + m₁ <• (0 : R) = 0 by rw [zero_smul, zero_add, op_zero, zero_smul]

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