English
The carrier of mem_carrier is equal to the underlying set membership; i.e., the carrier of the substructure equals the set it contains.
Русский
Носитель мембрера равен базовому множеству; носитель подпредставления равен множеству, которое оно содержит.
LaTeX
$$mem_carrier {s : NonUnitalStarSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s$$
Lean4
/-- The actual `NonUnitalStarSubsemiring` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass` and `StarMemClass`. -/
@[simps]
def ofClass {S R : Type*} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R] [NonUnitalSubsemiringClass S R]
[StarMemClass S R] (s : S) : NonUnitalStarSubsemiring R
where
carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
mul_mem' := mul_mem
star_mem' := star_mem
