copy — Mathlib

English

The copy of a Subring with a new carrier equal to the old one yields the same Subring.

Русский

Копия Subring с новым носителем, совпадающим с исходным, равна исходному Subring.

LaTeX

$$$ S.copy\\, s\\, hs = S $$$

Lean4

/-- Copy of a subring with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps coe toSubsemiring]
protected def copy (S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R :=
  { S.toSubsemiring.copy s hs with
    carrier := s
    neg_mem' := hs.symm ▸ S.neg_mem' }

Похожие утверждения