smul_inf

Mathlib.Algebra.Group.Subgroup.Pointwise

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

English

The scalar action distributes over intersection: a · (S ∩ T) = (a · S) ∩ (a · T).

Русский

Скалярное действие распределяется по пересечению: a · (S ∩ T) = (a · S) ∩ (a · T).

LaTeX

$$$ a \cdot (S \cap T) = (a \cdot S) \cap (a \cdot T) $$$

Lean4

@[simp]
theorem smul_inf (a : α) (S T : Subgroup G) : a • (S ⊓ T) = a • S ⊓ a • T := by
  simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

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

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

Разделы

Аффилиация

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