instNonUnitalSemiring — Mathlib

English

Submodules of an R-module form a NonUnitalSemiring under multiplication.

Русский

Подмодули R-модуля образуют неупорядоченное полукольцо под умножением.

LaTeX

$$$ \text{NonUnitalSemiring} (Submodule R A)$$$

Lean4

/-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/
instance : NonUnitalSemiring (Submodule R A)
    where
  __ := toAddSubmonoid_injective.semigroup _ mul_toAddSubmonoid
  zero_mul := bot_mul
  mul_zero := mul_bot
  left_distrib := mul_sup
  right_distrib := sup_mul

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