nontrivial_span_singleton

Mathlib.LinearAlgebra.Span.Defs

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

← MathLib Explorer

English

If x ≠ 0, then the span R∙x is nontrivial.

Русский

Если x ≠ 0, то подмодуль R∙x не тривиален.

LaTeX

$$$$ x \\neq 0 \\Rightarrow \\operatorname{Nontrivial}(R \\cdot x). $$$$

Lean4

theorem nontrivial_span_singleton {x : M} (h : x ≠ 0) : Nontrivial (R ∙ x) :=
  ⟨by
    use 0, ⟨x, Submodule.mem_span_singleton_self x⟩
    intro H
    rw [eq_comm, Submodule.mk_eq_zero] at H
    exact h H⟩

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

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

Разделы

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

Аффилиация

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