English
Given a set s ⊆ R, a subsemigroup sm with carrier s, and an additive subgroup sa with carrier s, the constructed NonUnitalSubring mk' s sm sa hm ha has as carrier s, and its subsemigroup and additive subgroup components are precisely sm and sa respectively.
Русский
Пусть имеется множество s ⊆ R, подполугруппа sm с переносом в s и аддитивная подгруппа sa с переносом в s; построенное ненадлежащее подпкольцо mk' s sm sa hm ha имеет носитель s, а соответственно подпполугруппа и аддитивная подгруппа равны sm и sa.
LaTeX
$$$\forall R\,[\text{NonUnitalNonAssocRing } R],\forall s\subseteq R,\forall sm,sa,\ hm:↑sm = s, ha:↑sa = s,\ (\text{NonUnitalSubring.mk'}\, s\ sm\ sa\ hm\ ha).toSubsemigroup = sm \land (\text{NonUnitalSubring.mk'}\, s\ sm\ sa\ hm\ ha).toAddSubgroup = sa \land ↑(\text{NonUnitalSubring.mk'}\, s\ sm\ sa\ hm\ ha) = s.$$$
Lean4
/-- Construct a `NonUnitalSubring R` from a set `s`, a subsemigroup `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
protected def mk' (s : Set R) (sm : Subsemigroup R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) :
NonUnitalSubring R :=
{ sm.copy s hm.symm, sa.copy s ha.symm with }
