English
There is a canonical copy of a subalgebra with a new carrier equal to the old one, preserving all algebraic data, so that the copy equals the original when the carrier matches.
Русский
Существует каноническая копия подалгебры с новым носителем, равным старому, сохраняющая все алгебраические данные; такая копия равна исходной при совпадении носителей.
LaTeX
$$$ \mathrm{copy}(S, s, hs) = S $, когда $s = \uparrow S$$$
Lean4
/-- Copy of a subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps coe toSubsemiring]
protected def copy (S : Subalgebra R A) (s : Set A) (hs : s = ↑S) : Subalgebra R A :=
{ S.toSubsemiring.copy s hs with
carrier := s
algebraMap_mem' := hs.symm ▸ S.algebraMap_mem' }
