English
Copy of a nonunital subring S to a new carrier set s with hs: s = ↑S yields a new NonUnitalSubring whose carrier is s and with the same structure as S.
Русский
Копия неединичного подполья S на новое множество-носитель s с доказательством hs: s = ↑S образует новое NonUnitalSubring с носителем s и той же структурой, что и S.
LaTeX
$$Definition: NonUnitalSubring.copy (S) (s) (hs) : NonUnitalSubring R$$
Lean4
/-- Copy of a non-unital subring with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubring R :=
{ S.toNonUnitalSubsemiring.copy s hs with
carrier := s
neg_mem' := hs.symm ▸ S.neg_mem' }
