span_eq

Mathlib.LinearAlgebra.Basis.Basic

URI: https://scilib.ai/kg/mathlib#Module.Basis.span_eq

English

The span of range b is the whole module; i.e., span R (range b) = ⊤, meaning b spans M.

Русский

Область span диапазона b равна ⊤, то есть b порождает весь модуль M.

LaTeX

$$$\operatorname{span} R (\operatorname{range} b) = \top$.$$

Lean4

@[simp]
protected theorem span_eq : span R (range b) = ⊤ :=
  eq_top_iff.mpr fun x _ => b.mem_span x

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

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

Разделы

Аффилиация

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