copy_eq

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.copy_eq

English

Equality of copies with the same carrier yields the identical subalgebra.

Русский

Равенство копий при одинаковом носителе приводит к равенству подалгебр.

LaTeX

$$$S.copy s hs = S$$$

Lean4

theorem copy_eq (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru