English
There is a StarMemClass instance for StarSubalgebra, i.e., star-membership is preserved.
Русский
Существует экземпляр StarMemClass для StarSubalgebra, т.е. сохранение принадлежности к звезде сохраняется.
LaTeX
$$$\\text{StarMemClass}(\\text{StarSubalgebra}(R,A),A)$$$
Lean4
/-- The actual `StarSubalgebra` obtained from an element of a type satisfying `SubsemiringClass`,
`SMulMemClass` and `StarMemClass`. -/
@[simps]
def ofClass {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A]
[SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A] (s : S) : StarSubalgebra R A
where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
mul_mem' := mul_mem
one_mem' := one_mem _
algebraMap_mem' := algebraMap_mem s
star_mem' := star_mem
