English
From a set, a submonoid, and an additive subgroup with compatible carriers one builds a Subring.
Русский
Из множества, подмоноида и аддитивной подгруппы с совместимыми носителями строится подкольцо.
LaTeX
$$$ (s : Set R) \\ (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R $$$
Lean4
/-- Construct a `Subring R` from a set `s`, a submonoid `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
@[simps! coe]
protected def mk' (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R :=
{ sm.copy s hm.symm, sa.copy s ha.symm with }
