span_singleton_mul_left_unit

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.span_singleton_mul_left_unit

English

If a is a unit, then span({a x}) = span({x}).

Русский

Если a является единицей, то span( {a x} ) = span( {x} ).

LaTeX

$$$\\text{If } a \\text{ is a unit},\\; \\operatorname{span}(\\{a x\\}) = \\operatorname{span}(\\{x\\})$$$

Lean4

theorem span_singleton_mul_left_unit {a : α} (h2 : IsUnit a) (x : α) : span ({a * x} : Set α) = span { x } :=
  Submodule.span_singleton_smul_eq h2 x

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

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

Разделы

Аффилиация

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