copy — Mathlib

English

Copying a submonoid along an equal carrier yields the same submonoid.

Русский

Копирование подмономиода вдоль эквивалентного носителя даёт тот же подмономиод.

LaTeX

$$$$ S\\,copy\\, s\\, hs = S $$$$

Lean4

/-- Copy a submonoid replacing `carrier` with a set that is equal to it. -/
@[to_additive /-- Copy an additive submonoid replacing `carrier` with a set that is equal to it. -/
    ]
protected def copy (S : Submonoid M) (s : Set M) (hs : s = S) : Submonoid M
    where
  carrier := s
  one_mem' := show 1 ∈ s from hs.symm ▸ S.one_mem'
  mul_mem' := hs.symm ▸ S.mul_mem'

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