copy — Mathlib

English

Copying a submodule to a new carrier equal to the old one yields the same submodule.

Русский

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

LaTeX

$$S.copy s hs = S$$

Lean4

/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps]
protected def copy (p : Submodule R M) (s : Set M) (hs : s = ↑p) : Submodule R M
    where
  carrier := s
  zero_mem' := by simp [hs]
  add_mem' := hs.symm ▸ p.add_mem'
  smul_mem' := by simpa [hs] using p.smul_mem'

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