instSubsingleton — Mathlib

English

If M is a Subsingleton, then LocalizedModule S M is a Subsingleton, giving an instance of subsingleton structure on the localized module.

Русский

Если M является субодиночным, то LocalizedModule S M является субодиночным и существует соответствующая инстанца.

LaTeX

$$$\text{Subsingleton}(M) \Rightarrow \text{Subsingleton}(\mathrm{LocalizedModule}\;S\;M)$$$

Lean4

instance [Subsingleton M] (S : Submonoid R) : Subsingleton (LocalizedModule S M) :=
  by
  rw [IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)]
  intro
  use 1, S.one_mem, Subsingleton.elim _ _

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