range_smul_range

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.range_smul_range

← MathLib Explorer

English

range b • range c = range (p ↦ b p.1 • c p.2)

Русский

range b • range c = range (p ↦ b p.1 • c p.2)

LaTeX

$$$ \\mathrm{range}\\, b \\cdot \\mathrm{range}\\, c = \\mathrm{range}\\, (\\lambda p: (b\\; p.1) \\cdot (c\\; p.2)) $$$

Lean4

@[to_additive]
theorem range_smul_range {ι κ : Type*} [SMul α β] (b : ι → α) (c : κ → β) :
    range b • range c = range fun p : ι × κ ↦ b p.1 • c p.2 :=
  image2_range ..

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

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

Разделы

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

Аффилиация

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