copy — Mathlib

English

Copying a SubMulAction with a new carrier equal to the old one yields the same object up to equality of carriers.

Русский

Копирование SubMulAction с новой носителем, равной старой, даёт тот же объект по тождению носителей.

LaTeX

$$$p.copy s hs = p$$$

Lean4

/-- Copy of a sub_mul_action with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive /-- Copy of a sub_mul_action with a new `carrier` equal to the old one.
      Useful to fix definitional equalities. -/
    ]
protected def copy (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : SubMulAction R M
    where
  carrier := s
  smul_mem' := hs.symm ▸ p.smul_mem'

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