mulOneClass — Mathlib

English

Canonical R-linear inclusion M → tsze_R M is given by inr.

Русский

Каноническое R-линейное вложение M → tsze_R M задаётся через inr.

LaTeX

$$$\mathrm{inrHom} : M \to_{\mathrm{R}} \mathrm{tsze}_{R} M \quad (\text{toFun} := \mathrm{inr})$$$

Lean4

instance mulOneClass [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
    MulOneClass (tsze R M) :=
  { TrivSqZeroExt.one,
    TrivSqZeroExt.mul with
    one_mul := fun x =>
      ext (one_mul x.1) <| show (1 : R) •> x.2 + (0 : M) <• x.1 = x.2 by rw [one_smul, smul_zero, add_zero]
    mul_one := fun x =>
      ext (mul_one x.1) <| show x.1 • (0 : M) + x.2 <• (1 : R) = x.2 by rw [smul_zero, zero_add, op_one, one_smul] }

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