copy — Mathlib

English

Copying a fractional ideal yields a fractional ideal with the same underlying submodule and set.

Русский

Копирование дробного идеала даёт дробный идеал с тем же подмодулем и тем же основанием.

LaTeX

$$$p.copy s hs$ preserves the underlying set$$

Lean4

/-- Copy of a `FractionalIdeal` with a new underlying set equal to the old one.
Useful to fix definitional equalities. -/
protected def copy (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p) : FractionalIdeal S P :=
  ⟨Submodule.copy p s hs, by
    convert p.isFractional
    ext
    simp only [hs]
    rfl⟩

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