range_smul'

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#LinearMap.range_smul'

English

For a nonzero scalar a, range(a • f) = range f.

Русский

Для неабсолютно нулевого скаляра a, диапазон a • f равен диапазону f.

LaTeX

$$$a \neq 0 \Rightarrow \operatorname{range}(a \cdot f) = \operatorname{range} f$$$

Lean4

theorem range_smul' (f : V →ₗ[K] V₂) (a : K) : range (a • f) = ⨆ _ : a ≠ 0, range f := by
  simpa only [range_eq_map] using Submodule.map_smul' f _ a

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

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

Разделы

Аффилиация

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