copy — Mathlib

English

Copy of a nonunital subsemiring with a new carrier equal to the old one; preserving the added structure.

Русский

Другая копия неединичного подполья с носителем, равным старому; сохраняет структуру.

LaTeX

$$NonUnitalSubsemiring.copy (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubsemiring R$$

Lean4

/-- Copy of a non-unital subsemiring with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubsemiring R :=
  { S.toAddSubmonoid.copy s hs, S.toSubsemigroup.copy s hs with carrier := s }

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