instNonUnitalSubsemiringClass — Mathlib

English

The star-closure property extends to the ambient NonUnitalStarSubalgebra structure, making StarMemClass applicable to NonUnitalStarSubalgebra.

Русский

Свойство звезды сохраняется и распространяется на структуру NonUnitalStarSubalgebra через StarMemClass.

LaTeX

$$$\\text{StarMemClass }(\\text{NonUnitalStarSubalgebra } R A) A$$$

Lean4

instance instNonUnitalSubsemiringClass : NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A
    where
  add_mem {s} := s.add_mem'
  mul_mem {s} := s.mul_mem'
  zero_mem {s} := s.zero_mem'

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