subsemiringClass — Mathlib

English

There is a canonical instance making StarSubsemiring into a SubsemiringClass over R, i.e., closed under addition, multiplication, with 0,1 in carrier.

Русский

Существует канонический экземпляр, делающий StarSubsemiring над R подслоем Subsemiring: замыкание по сложению, умножению, наличие 0 и 1 в носителе.

LaTeX

$$$\text{StarSubsemiring}.\text{subsemiringClass}$$$

Lean4

instance subsemiringClass : SubsemiringClass (StarSubsemiring R) R
    where
  add_mem {s} := s.add_mem'
  mul_mem {s} := s.mul_mem'
  zero_mem {s} := s.zero_mem'
  one_mem {s} := s.one_mem'

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