inlHom — Mathlib

English

The map inl: R → tsze_R M is a ring homomorphism, i.e., it preserves addition and multiplication and sends 1 to 1 and 0 to 0.

Русский

Отображение inl: R → tsze_R M является кольцевым гомоморфизмом: сохраняет сложение и умножение, единицу и ноль.

LaTeX

$$$ inl: R \\to tsze_R M \\text{ is a ring homomorphism}$$$

Lean4

/-- The canonical inclusion of rings `R → TrivSqZeroExt R M`. -/
@[simps apply]
def inlHom [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : R →+* tsze R M
    where
  toFun := inl
  map_one' := inl_one M
  map_mul' := inl_mul M
  map_zero' := inl_zero M
  map_add' := inl_add M

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