coe_toZModSubmodule

Mathlib.Algebra.Module.ZMod

URI: https://scilib.ai/kg/mathlib#AddSubgroup.coe_toZModSubmodule

English

For any AddSubgroup S of M, the underlying set of the corresponding ZMod-submodule is exactly S.

Русский

Для любого подгруппы S аддитивной группы M множество, лежащее в подмодуле ZMod-структуры, совпадает с S.

LaTeX

$$$(toZModSubmodule(n)\,S : Set M) = S$$$

Lean4

@[simp]
theorem coe_toZModSubmodule (S : AddSubgroup M) : (toZModSubmodule n S : Set M) = S :=
  rfl

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

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

Разделы

Аффилиация

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