smul_top

Mathlib.LinearAlgebra.AffineSpace.Pointwise

URI: https://scilib.ai/kg/mathlib#AffineSubspace.smul_top

← MathLib Explorer

English

If a is a unit, scaling the top (the whole space) preserves the top.

Русский

Если a — единица, умножение верха сохраняет верх.

LaTeX

$$$ a \\cdot (\\top : AffineSubspace k V) = \\top $$$

Lean4

@[simp]
theorem smul_top (ha : IsUnit a) : a • (⊤ : AffineSubspace k V) = ⊤ := by ext x;
  simpa [smul_eq_map, map_top] using ⟨ha.unit⁻¹ • x, smul_inv_smul ha.unit _⟩

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

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

Разделы

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

Аффилиация

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