copy_eq

Mathlib.Algebra.Module.Submodule.Defs

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

English

Equality of the copy map given a carrier equality implies the copy equals the original.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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