English
The instance asserts that NonUnitalStarSubsemiring R forms a NonUnitalSubsemiringClass with the base ring R, i.e., closure under addition, multiplication, and zero is inherited.
Русский
Инстанс утверждает, что NonUnitalStarSubsemiring R образует NonUnitalSubsemiringClass над R, то есть замкнутость по сложению, умножению и нулю наследуется.
LaTeX
$$NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass$$
Lean4
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is a non-unital commutative ring.
See note [reducible non-instances]. -/
abbrev adjoinNonUnitalCommRingOfComm (R : Type*) {A : Type*} [CommRing R] [StarRing R] [NonUnitalRing A] [StarRing A]
[Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s : Set A}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) :
NonUnitalCommRing (adjoin R s) :=
{ (adjoin R s).toNonUnitalRing, adjoinNonUnitalCommSemiringOfComm R hcomm hcomm_star with }
