inr_mul — Mathlib

English

For a1, a2 ∈ A, the product in Unitization of their images equals the image of their product; i.e., inr(a1) · inr(a2) = inr(a1 a2).

Русский

Для a1, a2 ∈ A произведение их изображений в Unitization равно изображению их произведения: inr(a1) · inr(a2) = inr(a1 a2).

LaTeX

$$$\mathrm{inr}(a_1) \cdot \mathrm{inr}(a_2) = \mathrm{inr}(a_1 a_2).$$$

Lean4

@[simp]
theorem inr_mul [MulZeroClass R] [AddZeroClass A] [Mul A] [SMulWithZero R A] (a₁ a₂ : A) :
    (↑(a₁ * a₂) : Unitization R A) = a₁ * a₂ :=
  ext (mul_zero _).symm <| show a₁ * a₂ = (0 : R) • a₂ + (0 : R) • a₁ + a₁ * a₂ by simp only [zero_smul, zero_add]

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