copy — Mathlib

English

Copying a subfield with the same carrier recovers the original subfield.

Русский

Копирование подполе с тем же носителем восстанавливает исходное подполе.

LaTeX

$$S.copy s hs = S$$

Lean4

/-- Copy of a subfield with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (S : Subfield K) (s : Set K) (hs : s = ↑S) : Subfield K :=
  { S.toSubring.copy s hs with
    carrier := s
    inv_mem' := hs.symm ▸ S.inv_mem' }

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