smul_bot

Mathlib.LinearAlgebra.AffineSpace.Pointwise

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

English

Scaling the bottom (empty?) affine subspace by any a yields the bottom.

Русский

Умножение нижнего подпполнения на любой a даёт нижнее.

LaTeX

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

Lean4

@[simp]
theorem smul_bot (a : M) : a • (⊥ : AffineSubspace k V) = ⊥ := by ext; simp [smul_eq_map, map_bot]

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

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

Разделы

Аффилиация

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