English
A copy of a subgroup with a new carrier equal to the old one yields a subgroup with the same carrier.
Русский
Копия подгруппы с новым носителем, равным старому, образует подгруппу с тем же носителем.
LaTeX
$$$\\text{copy}(K,s,hs) \\text{ is a subgroup with } \\operatorname{carrier} = s$$$
Lean4
/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive (attr := simps) /-- Copy of an additive subgroup with a new `carrier` equal to the old one.
Useful to fix definitional equalities -/
]
protected def copy (K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G
where
carrier := s
one_mem' := hs.symm ▸ K.one_mem'
mul_mem' := hs.symm ▸ K.mul_mem'
inv_mem' hx := by simpa [hs] using hx
