smul_bot

Mathlib.Algebra.Group.Subgroup.Pointwise

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

English

The action by any scalar on the bottom (trivial) subgroup of G yields the bottom subgroup: a · ⊥ = ⊥.

Русский

Действие скаляра на нулевую (тривиальную) подгруппу G оставляет её неизменной: a · ⊥ = ⊥.

LaTeX

$$$ a \cdot \bigl( \perp : Subgroup G \bigr) = \perp $$$

Lean4

@[simp]
theorem smul_bot (a : α) : a • (⊥ : Subgroup G) = ⊥ :=
  map_bot _

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

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

Разделы

Аффилиация

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