copy — Mathlib

English

Copy of a NonUnitalSubalgebra S with carrier s = ↑S yields a nonunital subalgebra with the same structure.

Русский

Копия ненулевой подпалгебры S с карриером s = ↑S сохраняет ту же структуру.

LaTeX

$$$\text{copy}(S, s, hs) = S$$$

Lean4

/-- Copy of a non-unital subalgebra with a new `carrier` equal to the old one.
Useful to fix definitional equalities. -/
protected def copy (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : NonUnitalSubalgebra R A :=
  { S.toNonUnitalSubsemiring.copy s hs with smul_mem' r a := by simpa [hs] using S.smul_mem r }

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