addSubgroup — Mathlib

English

Let M act on an additive group α by a distributive action. The subset of α consisting of elements fixed by every m ∈ M is an additive subgroup of α.

Русский

Пусть M действует на аддитивной группе α распределённо. Подмножество фиксированных элементов по всем m ∈ M образует аддитивную подпгруппу α.

LaTeX

$$$\\{a \\in \\alpha \\mid \\forall m \\in M,\\ m \\cdot a = a\\}$ является подгруппой по операции сложения на α.$$

Lean4

/-- The additive subgroup of elements fixed under the whole action. -/
def addSubgroup : AddSubgroup α where
  __ := addSubmonoid M α
  neg_mem' ha _ := by rw [smul_neg, ha]

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