English
From a set s, a subsemigroup sg, and an additive submonoid sa that all agree with s, one can form a nonunital subsemiring whose carrier is s and whose subsemigroup and submonoid structures come from sg and sa respectively.
Русский
Из множества s, подполугруппы sg и аддитивного подмоноида sa, совпадающих с s, существует неединичный подполнуг,Carrier которого равен s и члены sg, sa задают умножение и сложение.
LaTeX
$$If s : Set R, sg : Subsemigroup R with ↑sg = s, and sa : AddSubmonoid R with ↑sa = s, then there exists NonUnitalSubsemiring R with carrier s and with toSubsemigroup = sg and toAddSubmonoid = sa.$$
Lean4
/-- Construct a `NonUnitalSubsemiring R` from a set `s`, a subsemigroup `sg`, and an additive
submonoid `sa` such that `x ∈ s ↔ x ∈ sg ↔ x ∈ sa`. -/
protected def mk' (s : Set R) (sg : Subsemigroup R) (hg : ↑sg = s) (sa : AddSubmonoid R) (ha : ↑sa = s) :
NonUnitalSubsemiring R where
carrier := s
zero_mem' := by subst ha; exact sa.zero_mem
add_mem' := by subst ha; exact sa.add_mem
mul_mem' := by subst hg; exact sg.mul_mem
