mem_addSubmonoid — Mathlib

English

An element a of α belongs to the fixed-point submonoid if and only if a is fixed by every element of M, i.e., a ∈ addSubmonoid M α iff ∀ m ∈ M, m • a = a.

Русский

Элемент a принадлежит фиксированному подмонойду тогда и только тогда, когда каждый m ∈ M фиксирует a: a ∈ addSubmonoid M α эквивалентно ∀ m ∈ M, m • a = a.

LaTeX

$$$a \\in \\text{addSubmonoid } M \\alpha \\;\\Leftrightarrow\\; \\forall m \\in M,\\ m \\cdot a = a$$$

Lean4

@[simp]
theorem mem_addSubmonoid (a : α) : a ∈ addSubmonoid M α ↔ ∀ m : M, m • a = a :=
  Iff.rfl

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