English
If x belongs to the subsemiring mk from certain data, then x belongs to the chosen set.
Русский
Если x принадлежит подпол semiring mk из данных, то x принадлежит заданному множеству.
LaTeX
$$x ∈ mk {toSubmonoid} {add_mem} {zero_mem} ↔ x ∈ toSubmonoid$$
Lean4
/-- Construct a `Subsemiring R` from a set `s`, a submonoid `sm`, and an additive
submonoid `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
@[simps coe]
protected def mk' (s : Set R) (sm : Submonoid R) (hm : ↑sm = s) (sa : AddSubmonoid R) (ha : ↑sa = s) : Subsemiring R
where
carrier := s
zero_mem' := by exact ha ▸ sa.zero_mem
one_mem' := by exact hm ▸ sm.one_mem
add_mem' {x y} := by simpa only [← ha] using sa.add_mem
mul_mem' {x y} := by simpa only [← hm] using sm.mul_mem
