bot_lt_isotypicComponents

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#bot_lt_isotypicComponents

← MathLib Explorer

English

If m is in the set of all isotypic components, then m is nontrivial: ⊥ < m.

Русский

Если m принадлежит множеству компонент изотипичности, то m непустой: ⊥ < m.

LaTeX

$$$\bot < m$ for $m \in \text{isotypicComponents}(R, M)$$$

Lean4

theorem bot_lt_isotypicComponents {m : Submodule R M} (h : m ∈ isotypicComponents R M) : ⊥ < m := by
  obtain ⟨_, _, rfl⟩ := h; exact bot_lt_isotypicComponent ..

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

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

Разделы

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

Аффилиация

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