English
The collection of NonUnitalStarSubalgebras forms a NonUnitalSubsemiringClass, i.e., closed under addition and multiplication in A.
Русский
Коллекция неунициализированных звёздных подалгебр образует класс NonUnitalSubsemiringClass: замкнута по сложению и умножению внутри A.
LaTeX
$$$\\text{NonUnitalSubsemiringClass }(\\text{NonUnitalStarSubalgebra } R A) A$$$
Lean4
/-- The actual `NonUnitalStarSubalgebra` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass`, `SMulMemClass` and `StarMemClass`. -/
@[simps]
def ofClass {S R A : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [SetLike S A]
[NonUnitalSubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A] (s : S) : NonUnitalStarSubalgebra R A
where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
mul_mem' := mul_mem
smul_mem' := SMulMemClass.smul_mem
star_mem' := star_mem
