carrier_eq_coe

Mathlib.Algebra.Module.Submodule.Defs

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

English

For any submodule S ⊆ M, the carrier set of S coincides with the underlying set of S.

Русский

Для подмодуля S ⊆ M носитель множества совпадает с базовым множеством S.

LaTeX

$$$\\operatorname{carrier}(S) = S$$$

Lean4

@[simp]
theorem carrier_eq_coe (s : Submodule R M) : s.carrier = s :=
  rfl

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

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

Разделы

Аффилиация

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