generators_mem

Mathlib.Algebra.Module.SpanRank

URI: https://scilib.ai/kg/mathlib#Submodule.FG.generators_mem

← MathLib Explorer

English

Every generator in generators(p) lies in p; generators(p) ⊆ p.

Русский

Каждый порождающий в generators(p) принадлежит p; generators(p) ⊆ p.

LaTeX

$$$\mathrm{generators}(p) \subseteq p.$$$

Lean4

/-- The elements of the generators are in the submodule. -/
theorem generators_mem (p : Submodule R M) : generators p ⊆ p :=
  by
  nth_rw 2 [← span_generators p]
  exact subset_span (s := generators p)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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