subsingleton — Mathlib

English

A module M over a Subsingleton semiring is itself a Subsingleton.

Русский

Модуль M над одноэлементной полугруппой является одноэлементным.

LaTeX

$$$\\text{Subsingleton } M$$$

Lean4

/-- A module over a `Subsingleton` semiring is a `Subsingleton`. We cannot register this
as an instance because Lean has no way to guess `R`. -/
protected theorem subsingleton (R M : Type*) [MonoidWithZero R] [Subsingleton R] [Zero M] [MulActionWithZero R M] :
    Subsingleton M :=
  MulActionWithZero.subsingleton R M

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